instProperSpace — Mathlib

English

The upper half-plane ℍ, with its natural metric, is a proper space: every closed ball is compact (equivalently, closed balls are compact in ℍ).

Русский

Верхняя полуплоскость ℍ с естественной метрикой является правильным пространством: для любого z ∈ ℍ и r ≥ 0 замкнутый шар компактнен.

LaTeX

$$$$ \\text{For all } z \\in \\mathbb{H}, \\ \\overline{B}_{\\mathbb{H}}(z,r) \\text{ is compact for all } r \\ge 0. $$$$

Lean4

instance : ProperSpace ℍ := by
  refine ⟨fun z r => ?_⟩
  rw [IsInducing.subtypeVal.isCompact_iff (f := ((↑) : ℍ → ℂ)), image_coe_closedBall]
  apply isCompact_closedBall

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