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