instProperSpace — Mathlib

English

NNReal is a proper space: the embedding into ℝ preserves compactness of closed balls.

Русский

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

LaTeX

$$$\text{ProperSpace}(\mathbb{R}_{\ge 0})$$$

Lean4

instance instProperSpace : ProperSpace ℝ≥0 where
  isCompact_closedBall x
    r := by
    have emb : IsClosedEmbedding ((↑) : ℝ≥0 → ℝ) := Isometry.isClosedEmbedding fun _ ↦ congrFun rfl
    exact emb.isCompact_preimage (K := Metric.closedBall x r) (isCompact_closedBall _ _)

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