instProperSpace — Mathlib

English

For every center n and radius r, the closed ball is compact; equivalently, ℕ is a proper metric space.

Русский

Для каждого центра n и радиуса r замкнутый шар компакт; то есть ℕ — это правильное метрическое пространство.

LaTeX

$$$\forall n\in\mathbb{N},\forall r\in\mathbb{R},\quad \operatorname{IsCompact}(\operatorname{closedBall}(n,r))$$$

Lean4

instance : ProperSpace ℕ :=
  ⟨fun x r => by
    rw [closedBall_eq_Icc]
    exact (Set.finite_Icc _ _).isCompact⟩

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