English
Let a and b be integers. Then the open interval Ioo(a,b) consists exactly of the integers a+1, a+2, ..., b−1; hence Ioo(a,b) is finite and indexable by natural numbers via k ↦ a+1+k, giving an explicit bijection with the initial segment {0,1,..., (b−a−1).toNat − 1}. In particular, |Ioo(a,b)| = max(0, b−a−1).
Русский
Пусть a и b — целые числа. Тогда открытый интервал Ioo(a,b) состоит ровно из целых чисел a+1, a+2, ..., b−1; следовательно Ioo(a,b) конечно и обладает явной биекцией с начальным отрезком натуральных чисел через k ↦ a+1+k, где k принимает значения от 0 до (b−a−1).toNat−1. По мере необходимости кардиналность |Ioo(a,b)| равна max(0, b−a−1).
LaTeX
$$$\\lvert Ioo(a,b)\\rvert = \\max\\{0,\, b - a - 1\\}$ and $Ioo(a,b) = \\{a+1, a+2, \\dots, b-1\\}$, with the indexing $k \\mapsto a+1+k$ from $\\{0,1,\\dots, (b-a-1).toNat-1\\}$.$$
Lean4
theorem Ioo_eq_finset_map :
Ioo a b = (Finset.range (b - a - 1).toNat).map (Nat.castEmbedding.trans <| addLeftEmbedding (a + 1)) :=
rfl
