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