Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separated_iff_disjoint

Modification history

2022-09-27 17:24
src/topology/separation.lean
chore(topology/separation): rename `separated` to `separated_nhds` (#16604) …
Deleted separated_iff_disjointView on Github →
2022-09-17 16:29
src/topology/separation.lean
feat(topology/separation): define `T₅` spaces (#16533) …
Added separated_iff_disjointView on Github →