instIsOrderBornology — Mathlib

English

The natural numbers form an IsOrderBornology; i.e., they have the order-bornology property, since each finite closed interval Icc(a,b) is compact.

Русский

Натуральные числа образуют IsOrderBornology; свойство order-bornology, так как каждый конечный замкнутый отрезок Icc(a,b) компактен.

LaTeX

$$$\operatorname{IsOrderBornology}(\mathbb{N})$$$

Lean4

instance : IsOrderBornology ℕ :=
  .of_isCompactIcc 0 (by simp) (by simp [Nat.closedBall_eq_Icc])

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