instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space

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 }

Похожие утверждения