emetric_space): `nhds_within` lemmas (#16952)

Commit

3 years ago

feat(topology/metric_space/emetric_space): `nhds_within` lemmas (#16952) A few lemmas about emetric spaces and `nhds_within`.

Author

YaelDillies

Parents