prod — Mathlib

English

The product of two completely metrizable spaces is completely metrizable.

Русский

Произведение двух полностью метризуемых пространств — полностью метризуемо.

LaTeX

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

Lean4

/-- The product of two completely metrizable spaces is completely metrizable. -/
instance prod [TopologicalSpace X] [IsCompletelyMetrizableSpace X] [TopologicalSpace Y]
    [IsCompletelyMetrizableSpace Y] : IsCompletelyMetrizableSpace (X × Y) :=
  letI := upgradeIsCompletelyMetrizable X
  letI := upgradeIsCompletelyMetrizable Y
  inferInstance

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