instMetrizableSpace — 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

instance : MetrizableSpace ENNReal :=
  orderIsoUnitIntervalBirational.toHomeomorph.isEmbedding.metrizableSpace

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