Mathlib v3 is deprecated. Go to Mathlib v4

Theorem totally_separated_space_of_t1_of_basis_clopen

Modification history

2022-09-14 08:28
src/topology/separation.lean
feat(topology/separation): generalize&rename a lemma (#16503) …
Added totally_separated_space_of_t1_of_basis_clopenView on Github →