range_eq_Icc_zero_sub_one — Mathlib

English

If n > 0, then the range n equals the closed interval from 0 to n−1.

Русский

Если n > 0, то диапазон n равен замкнутому отрезку [0, n−1].

LaTeX

$$$\forall n \in \mathbb{N},\ n \neq 0 \Rightarrow \operatorname{range}(n) = \operatorname{Icc}(0, n-1)$$$

Lean4

theorem range_eq_Icc_zero_sub_one (n : ℕ) (hn : n ≠ 0) : range n = Icc 0 (n - 1) :=
  by
  ext b
  simp_all only [mem_Icc, zero_le, true_and, mem_range]
  exact lt_iff_le_pred (zero_lt_of_ne_zero hn)

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