finsetImage_val_Ico — Mathlib

English

For a,b ∈ Fin n, the image of the Ico interval under the natural embedding is the Nat interval from a.val to b.val.

Русский

Для a,b ∈ Fin n образ Ico под естественным вложением даёт Nat-интервал от a.val до b.val.

LaTeX

$$$(\operatorname{Finset.Ico}\ a\ b).\mathrm{image}\ \mathrm{val} = \operatorname{Finset.Ico}(a.\mathrm{val}, b.\mathrm{val})$$$

Lean4

@[simp]
theorem finsetImage_val_Ico : (Ico a b).image val = Ico (a : ℕ) b :=
  image_val_attachFin _

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