Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separated.disjoint_closure_right

Modification history

2022-09-27 17:24
src/topology/separation.lean
chore(topology/separation): rename `separated` to `separated_nhds` (#16604) …
Deleted separated.disjoint_closure_rightView on Github →
2022-03-18 21:54
src/topology/separation.lean
feat(topology/{order,separation}): several lemmas from an old branch (#12794) …
Added separated.disjoint_closure_rightView on Github →