mathlib
5ef365a3 - feat(topology/separation): generalize tendsto_const_nhds_iff to t1_space (#12883)

Commit

3 years ago

feat(topology/separation): generalize tendsto_const_nhds_iff to t1_space (#12883) I noticed this when working on the sphere eversion project

Author

fpvandoorn

Parents