instLocallyFiniteOrder — Mathlib

English

The natural numbers with the usual order are locally finite: for all a ≤ b, the interval [a,b] is finite and contains exactly b − a + 1 elements.

Русский

Натуральные числа с обычным порядком локально конечны: для любых a ≤ b множество [a,b] конечно и содержит ровно b − a + 1 элементов.

LaTeX

$$\forall a,b ∈ \mathbb{N},\ a \le b \implies \#\{ x ∈ \mathbb{N} : a \le x \le b \} = b - a + 1$$

Lean4

instance instLocallyFiniteOrder : LocallyFiniteOrder ℕ
    where
  finsetIcc a b := ⟨List.range' a (b + 1 - a), List.nodup_range'⟩
  finsetIco a b := ⟨List.range' a (b - a), List.nodup_range'⟩
  finsetIoc a b := ⟨List.range' (a + 1) (b - a), List.nodup_range'⟩
  finsetIoo a b := ⟨List.range' (a + 1) (b - a - 1), List.nodup_range'⟩
  finset_mem_Icc a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega
  finset_mem_Ico a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega
  finset_mem_Ioc a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega
  finset_mem_Ioo a b x := by rw [Finset.mem_mk, Multiset.mem_coe, List.mem_range'_1]; omega

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