mathlib
a3bb2050 - feat(topology/separation): generalize&rename a lemma (#16503)

Commit
3 years ago
feat(topology/separation): generalize&rename a lemma (#16503) * rename `tot_sep_of_zero_dim` to `totally_separated_space_of_t1_of_basis_clopen`; * generalize it from a `t2_space` to a `t1_space`.
Author
Parents
Loading