English
The image of Ici i under natAdd m is Ici (natAdd m i).
Русский
Образ Ici i под natAdd m равен Ici (natAdd m i).
LaTeX
$$$\mathrm{Set.image}(\mathrm{Fin.natAdd}(m), \mathrm{Set.Ici}(i)) = \mathrm{Ici}(\mathrm{natAdd}(m,i))$$$
Lean4
@[simp]
theorem image_natAdd_Ici (m) (i : Fin n) : natAdd m '' Ici i = Ici (natAdd m i) :=
by
rw [← preimage_natAdd_Ici_natAdd, image_preimage_eq_of_subset]
rw [range_natAdd]
exact fun j hj ↦ Nat.le_trans (le_coe_natAdd ..) hj