instT2SpaceSum — Mathlib

English

If X and Y are Hausdorff spaces, then the disjoint sum X ⊕ Y is Hausdorff.

Русский

Если X и Y — Хаусдорфовы пространства, то их дизъюнктное объединение X ⊕ Y также Хаусдорфово.

LaTeX

$$$ [TopologicalSpace X] [T2Space X] [TopologicalSpace Y] [T2Space Y] \\Rightarrow T2Space(X \\oplus Y)$$$

Lean4

instance [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X ⊕ Y) :=
  by
  constructor
  rintro (x | x) (y | y) h
  · exact separated_by_isOpenEmbedding .inl <| ne_of_apply_ne _ h
  · exact separated_by_continuous continuous_isLeft <| by simp
  · exact separated_by_continuous continuous_isLeft <| by simp
  · exact separated_by_isOpenEmbedding .inr <| ne_of_apply_ne _ h

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