English
For any Fin n and natural m>0 with NeZero m, the image of the infinite interval Ici i under castAdd m equals the half-open interval Ico (castAdd m i) (natAdd n 0).
Русский
При любом i ∈ Fin n и m>0 (NeZero m) образ Ici i под castAdd m равен Ico (castAdd m i) (natAdd n 0).
LaTeX
$$$ (\mathrm{Finset}.Ici\, i).image (\mathrm{Fin.castAdd}\, m) = \mathrm{Finset}.Ico\ (\mathrm{Fin.castAdd}\, m\, i) (\mathrm{Fin.natAdd}\, n\, 0) $$$
Lean4
@[simp]
theorem finsetImage_castAdd_Ici (m) [NeZero m] (i : Fin n) :
(Ici i).image (castAdd m) = Ico (castAdd m i) (natAdd n 0) := by simp [← coe_inj]