mathlib

e6f28f56 - feat(topology/algebra/order/basic): `nhds_within` versions (#16956)

feat(topology/algebra/order/basic): `nhds_within` versions (#16956) Version of `exists_seq_strict_mono_tendsto`/`exists_seq_strict_anti_tendsto` strengthened to `nhds_within`.