completeSpace

Mathlib.Topology.MetricSpace.Isometry

URI: https://scilib.ai/kg/mathlib#IsometryEquiv.completeSpace

English

If β is a complete space, then α is complete under an isometry e: α ≃ᵢ β.

Русский

Если β — полное пространство, то α тоже полное под изометрией e: α ≃ᵢ β.

LaTeX

$$$\text{CompleteSpace}(β) \Rightarrow \text{CompleteSpace}(α) \text{ for } e: α \simeq_i β$$$

Lean4

protected theorem completeSpace [CompleteSpace β] (e : α ≃ᵢ β) : CompleteSpace α :=
  e.completeSpace_iff.2 ‹_›

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

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

Разделы

Аффилиация

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