pseudoMetrizableSpace_prod — Mathlib

English

If X and Y are pseudo-metrizable, then their product X × Y is pseudo-metrizable.

Русский

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

LaTeX

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

Lean4

instance pseudoMetrizableSpace_prod [PseudoMetrizableSpace X] [PseudoMetrizableSpace Y] :
    PseudoMetrizableSpace (X × Y) :=
  letI : PseudoMetricSpace X := pseudoMetrizableSpacePseudoMetric X
  letI : PseudoMetricSpace Y := pseudoMetrizableSpacePseudoMetric Y
  inferInstance

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