t1Space_of_injective_of_continuous

English

If f : X → Y is an embedding and Y is a T1-space, then X is a T1-space.

Русский

Если отображение f: X → Y является вложением и Y — T1-пространство, то X также является T1-пространством.

LaTeX

$$$ \text{IsEmbedding}(f) \Rightarrow (\text{T1Space } Y) \Rightarrow \text{T1Space } X$ (with assumptions on topological spaces).$$

Lean4

theorem t1Space_of_injective_of_continuous [TopologicalSpace Y] {f : X → Y} (hf : Function.Injective f)
    (hf' : Continuous f) [T1Space Y] : T1Space X :=
  t1Space_iff_specializes_imp_eq.2 fun _ _ h => hf (h.map hf').eq

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