English
Let m ∈ ℕ and i, j ∈ Fin(n). The image of the half-open interval Ico(i, j) under the translation x ↦ x + m is exactly Ico(i + m, j + m).
Русский
Пусть m ∈ ℕ и i, j ∈ Fin(n). Образ полуоткрытого интервала Ico(i, j) при отображении x ↦ x + m равен Ico(i + m, j + m).
LaTeX
$$$$ \\\\mathrm{Set.image}(\\\\mathrm{Fin.natAdd}(m))(\\\\mathrm{Set.Ico}(i,j)) = \\\\mathrm{Set.Ico}(\\\\mathrm{Fin.natAdd}(m)i, \\\\mathrm{Fin.natAdd}(m)j). $$$$
Lean4
@[simp]
theorem image_natAdd_Ico (m) (i j : Fin n) : natAdd m '' Ico i j = Ico (natAdd m i) (natAdd m j) :=
by
rw [← preimage_natAdd_Ico_natAdd, image_preimage_eq_of_subset]
exact Ico_subset_Ici_self.trans <| image_natAdd_Ici m i ▸ image_subset_range _ _
