of_injective_continuous — Mathlib

English

If f: X → Y is injective and continuous and Y is Hausdorff, then X is Hausdorff.

Русский

Пусть f: X → Y будет инъективной и непрерывной, Y — Хаусдорфово пространство; тогда X тоже Хаусдорфово.

LaTeX

$$$ \\forall X\, Y\\,[TopologicalSpace\\ X]\\,[TopologicalSpace\\ Y]\\,[T2Space\\ Y],\\ f:X\\to Y,\\ (Injective(f) \\land Continuous(f)) \\Rightarrow T2Space(X)$$$

Lean4

/-- If the codomain of an injective continuous function is a Hausdorff space, then so is its
domain. -/
theorem of_injective_continuous [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hinj : Injective f) (hc : Continuous f) :
    T2Space X :=
  ⟨fun _ _ h => separated_by_continuous hc (hinj.ne h)⟩

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