Theorem ExtremallyDisconnected.disjoint_closure_of_disjoint_IsOpen

Modification history

2023-09-07 12:30
Mathlib/Topology/ExtremallyDisconnected.lean
chore: tidy various files (#7009)
Deleted ExtremallyDisconnected.disjoint_closure_of_disjoint_IsOpenView on Github →
2023-08-09 19:01
Mathlib/Topology/ExtremallyDisconnected.lean
feat(Topology/ExtremallyDisconnected): prove Gleason's theorem (#5634) …
Added ExtremallyDisconnected.disjoint_closure_of_disjoint_IsOpenView on Github →