instProperSpaceMultiplicative — Mathlib

English

If X is a metric space that is proper, then the multiplicative space Multiplicative X is proper.

Русский

Если X — метрическое пространство, являющееся правильным, то Multiplicative X является правильным пространством.

LaTeX

$$$[\\text{PseudoMetricSpace}(X)]\\ [\\text{ProperSpace}(X)]\\Rightarrow \\text{ProperSpace}(\\text{Multiplicative}(X))$$$

Lean4

instance [PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Multiplicative X) :=
  ‹ProperSpace X›

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