English
For any a,b in Fin n, mapping the Fin-set Icc(a,b) to natural numbers via the natural embedding yields the natural interval between a.val and b.val.
Русский
Для любых a,b ∈ Fin n отображение Finset Icc(a,b) в ℕ через естественное вложение даёт натуральный интервал между a.val и b.val.
LaTeX
$$$(\operatorname{Finset.Icc}\ a\ b).\mathrm{image}\ \mathrm{val} = \operatorname{Finset.Icc}(a.\mathrm{val}, b.\mathrm{val})$$$
Lean4
@[simp]
theorem finsetImage_val_Icc : (Icc a b).image val = Icc (a : ℕ) b :=
image_val_attachFin _