t2space_iff_isSeparatedMap — Mathlib

English

A space X is Hausdorff iff every constant map X→Y is a separated map (for any codomain Y).

Русский

Пространство Х является хаусдорфовым тогда и только тогда, когда любая константная карта X→Y является разделимой.

LaTeX

$$$$\\text{T2Space}(X) \\iff \\operatorname{IsSeparatedMap}(\\lambda x:X, y).$$$$

Lean4

theorem t2space_iff_isSeparatedMap (y : Y) : T2Space X ↔ IsSeparatedMap fun _ : X ↦ y :=
  ⟨fun ⟨t2⟩ _ _ _ hne ↦ t2 hne, fun sep ↦ ⟨fun x₁ x₂ hne ↦ sep x₁ x₂ rfl hne⟩⟩

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