t2Space — Mathlib

English

A totally separated space is Hausdorff (T2).

Русский

Полностью разделённое пространство — это т2-пространство (хаусдорфово).

LaTeX

$$TotallySeparatedSpace X → T2Space X$$

Lean4

/-- A totally separated space is T2. -/
instance t2Space [TotallySeparatedSpace X] : T2Space X where
  t2 x y
    h := by
    obtain ⟨u, v, h₁, h₂, h₃, h₄, _, h₅⟩ := isTotallySeparated_univ trivial trivial h
    exact ⟨u, v, h₁, h₂, h₃, h₄, h₅⟩

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