t1Space — Mathlib

English

If f is an embedding X → Y, and Y is a topological space with T1 separation, then X is T1.

Русский

Если отображение является вложением между X и Y, и Y — топологическое пространство с T1-разделением, то X — T1-пространство.

LaTeX

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

Lean4

protected theorem t1Space [TopologicalSpace Y] [T1Space Y] {f : X → Y} (hf : IsEmbedding f) : T1Space X :=
  t1Space_of_injective_of_continuous hf.injective hf.continuous

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