mathlib
be9a5dec - feat(topology/separation): add `t1_space_tfae` (#11534)

Commit

4 years ago

feat(topology/separation): add `t1_space_tfae` (#11534) Also add some lemmas about `filter.disjoint`.

Author

urkud

Parents