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`.





leanprover-community/mathlib,leanprover-community/mathlib