t2Space — Mathlib

English

If f is an embedding into a Hausdorff space Y, then X is Hausdorff.

Русский

Если f: X → Y — вложение в Хаусдорфово пространство Y, то X является Хаусдорфовым.

LaTeX

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

Lean4

/-- If the codomain of a topological embedding is a Hausdorff space, then so is its domain.
See also `T2Space.of_continuous_injective`. -/
theorem t2Space [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : IsEmbedding f) : T2Space X :=
  .of_injective_continuous hf.injective hf.continuous

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