metrizableSpace_prod — Mathlib

English

If X and Y are metrizable, then X × Y is metrizable.

Русский

Если X и Y метризуемы, то произведение X × Y метризуемо.

LaTeX

$$$[\text{MetrizableSpace } X] \land [\text{MetrizableSpace } Y] \Rightarrow [\text{MetrizableSpace } (X \times Y)]$$$

Lean4

instance metrizableSpace_prod [MetrizableSpace X] [MetrizableSpace Y] : MetrizableSpace (X × Y) :=
  letI : MetricSpace X := metrizableSpaceMetric X
  letI : MetricSpace Y := metrizableSpaceMetric Y
  inferInstance

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