sum — Mathlib

English

The disjoint union (sum) of two completely metrizable spaces is completely metrizable.

Русский

Расщепление по индексу двух полностью метризуемых пространств сохраняет метризуемость.

LaTeX

$$$\\forall X Y, [TopologicalSpace X] [IsCompletelyMetrizableSpace X] [TopologicalSpace Y] [IsCompletelyMetrizableSpace Y]\\Rightarrow IsCompletelyMetrizableSpace (X \\oplus Y)$$$

Lean4

/-- The disjoint union of two completely metrizable spaces is completely metrizable. -/
instance sum [TopologicalSpace X] [IsCompletelyMetrizableSpace X] [TopologicalSpace Y] [IsCompletelyMetrizableSpace Y] :
    IsCompletelyMetrizableSpace (X ⊕ Y) :=
  letI := upgradeIsCompletelyMetrizable X
  letI := upgradeIsCompletelyMetrizable Y
  inferInstance

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