t4Space — Mathlib

English

If f: X → Y is a closed embedding and Y is T4, then X is T4.

Русский

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

LaTeX

$$$ \\forall f:\\, X \\to Y,\\ IsClosedEmbedding f \\Rightarrow ( [T4Space Y] \\Rightarrow [T4Space X] )$$$

Lean4

/-- If the codomain of a closed embedding is a T₄ space, then so is the domain. -/
protected theorem t4Space [TopologicalSpace Y] [T4Space Y] {f : X → Y} (hf : IsClosedEmbedding f) : T4Space X
    where
  toT1Space := hf.isEmbedding.t1Space
  toNormalSpace := hf.normalSpace

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