English
If Y is completely normal and e: X → Y is an embedding, then X is completely normal.
Русский
Пусть Y — полностью нормальное пространство, и e: X → Y — вложение; тогда X тоже полностью нормальное.
LaTeX
$$$ \\text{IsEmbedding}(e) \\Rightarrow (\\text{CompletelyNormalSpace}(Y) \\Rightarrow \\text{CompletelyNormalSpace}(X))$$$
Lean4
theorem completelyNormalSpace [TopologicalSpace Y] [CompletelyNormalSpace Y] {e : X → Y} (he : IsEmbedding e) :
CompletelyNormalSpace X := by
refine ⟨fun s t hd₁ hd₂ => ?_⟩
simp only [he.isInducing.nhdsSet_eq_comap]
refine disjoint_comap (completely_normal ?_ ?_)
·
rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl, ← he.closure_eq_preimage_closure_image,
subset_compl_iff_disjoint_left]
·
rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl, ← he.closure_eq_preimage_closure_image,
subset_compl_iff_disjoint_right]
