instProperSpaceReal

Mathlib.Topology.MetricSpace.ProperSpace.Real

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

English

The real line ℝ is a proper space: every closed ball is compact.

Русский

Линия чисел ℝ — правильное пространство: каждый замкнутый шар компактен.

LaTeX

$$$\text{ProperSpace}(\mathbb{R})$$$

Lean4

instance : ProperSpace ℝ where
  isCompact_closedBall x
    r := by
    rw [Real.closedBall_eq_Icc]
    apply isCompact_Icc

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

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

Разделы

Аффилиация

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