finsetImage_val_Icc — Mathlib

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 _

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