English
Extremally disconnected spaces are totally separated provided they are also T2 spaces.
Русский
Экстремально разобщимые пространства являются полностью разделимыми при условии T2.
LaTeX
$$$$ \\text{If } X \\text{ is ExtremallyDisconnected and } X \\text{ is T2, then } X \\text{ is TotallySeparatedSpace}. $$$$
Lean4
/-- Extremally disconnected spaces are totally separated. -/
instance [ExtremallyDisconnected X] [T2Space X] : TotallySeparatedSpace X :=
{
isTotallySeparated_univ := by
intro x _ y _ hxy
obtain ⟨U, V, hUV⟩ := T2Space.t2 hxy
refine
⟨closure U, (closure U)ᶜ, ExtremallyDisconnected.open_closure U hUV.1, by
simp only [isOpen_compl_iff, isClosed_closure], subset_closure hUV.2.2.1, ?_, by
simp only [Set.union_compl_self, Set.subset_univ], disjoint_compl_right⟩
rw [Set.mem_compl_iff, mem_closure_iff]
push_neg
refine ⟨V, ⟨hUV.2.1, hUV.2.2.2.1, ?_⟩⟩
rw [← Set.disjoint_iff_inter_eq_empty, disjoint_comm]
exact hUV.2.2.2.2 }