English
Let a,b be integers. The inclusive interval uIcc(a,b) is exactly the set {min(a,b), min(a,b)+1, ..., max(a,b)}. There is an explicit bijection with the range {0,1,..., max(a,b)+1−min(a,b)−1} given by k ↦ min(a,b) + k, showing that uIcc(a,b) has length |a−b|+1.
Русский
Пусть a и b — целые числа. Инклюзивный интервал uIcc(a,b) равен множеству {min(a,b), min(a,b)+1, ..., max(a,b)}. Существует явная биекция с диапазоном {0,1, ..., max(a,b)−min(a,b)} через k ↦ min(a,b) + k, что показывает, что длина uIcc(a,b) равна |a−b|+1.
LaTeX
$$$uIcc(a,b) = \\{\\min(a,b), \\min(a,b)+1, \\dots, \\max(a,b)\\}$ and $|uIcc(a,b)| = |a-b|+1$ with the natural bijection $k \\mapsto \\min(a,b)+k$ from $\\{0,1,\\dots,|a-b|\\}$.$$
Lean4
theorem uIcc_eq_finset_map :
uIcc a b = (range (max a b + 1 - min a b).toNat).map (Nat.castEmbedding.trans <| addLeftEmbedding <| min a b) :=
rfl
