instProperSpaceAdditive — Mathlib

English

If X is a metric space that is proper, then the additive space Additive X is proper.

Русский

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

LaTeX

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

Lean4

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

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