English
If the codomain is normal and the embedding is closed, then the domain is normal.
Русский
Если кодом является нормальное пространство и вложение замкнуто, то домен нормален.
LaTeX
$$$\text{If } f: X\to Y \text{ is a closed embedding and } Y \text{ is NormalSpace},\; X \text{ is NormalSpace.}$$$
Lean4
/-- If the codomain of a closed embedding is a normal space, then so is the domain. -/
protected theorem normalSpace [TopologicalSpace Y] [NormalSpace Y] {f : X → Y} (hf : IsClosedEmbedding f) :
NormalSpace X where
normal s t hs ht
hst :=
by
have H : SeparatedNhds (f '' s) (f '' t) :=
NormalSpace.normal (f '' s) (f '' t) (hf.isClosedMap s hs) (hf.isClosedMap t ht)
(disjoint_image_of_injective hf.injective hst)
exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _)
