Iio_eq_range — Mathlib

English

For every natural number n, the Finset of numbers strictly less than n equals the initial segment {0,1,…,n−1}.

Русский

Для любого натурального числа n множество целых чисел, меньших n, совпадает с начальными членами {0,1,…,n−1}.

LaTeX

$$$\forall n \in \mathbb{N},\ Iio(n) = \operatorname{range}(n)$$$

Lean4

theorem Iio_eq_range : Iio = range := by
  ext b x
  rw [mem_Iio, mem_range]

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