normalSpace — Mathlib

English

Let h: X ≃ₜ Y be a homeomorphism between topological spaces. If X is a normal space, then Y is normal.

Русский

Пусть X и Y — топологические пространства, и h:X ≃ₜ Y — гомеоморфизм. Если X нормальное пространство, то Y нормальное.

LaTeX

$$$ \\forall X,Y\\ [TopologicalSpace X] [TopologicalSpace Y],\\ h:X\\simeq Y\\Rightarrow (NormalSpace X\\Rightarrow NormalSpace Y)$$$

Lean4

protected theorem normalSpace [TopologicalSpace Y] [NormalSpace X] (h : X ≃ₜ Y) : NormalSpace Y :=
  h.symm.isClosedEmbedding.normalSpace

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