instProperSpaceOrderDual

Mathlib.Topology.MetricSpace.ProperSpace

URI: https://scilib.ai/kg/mathlib#instProperSpaceOrderDual

English

If X is a proper metric space, then its order dual X^o is also proper.

Русский

Если X — правильное метрическое пространство, то его двойник порядка X^o также правильный.

LaTeX

$$$[\\text{PseudoMetricSpace}(X)]\\ [\\text{ProperSpace}(X)]\\Rightarrow \\text{ProperSpace}(X^{\\mathrm{op}})$$$

Lean4

instance [PseudoMetricSpace X] [ProperSpace X] : ProperSpace Xᵒᵈ :=
  ‹ProperSpace X›

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru