English
Let n ∈ ℕ and m ∈ ℕ, and i, j ∈ Fin(n). The image of the open-interval uIoo(i, j) under the translation x ↦ x + m equals the open-interval between i + m and j + m, i.e. the translation shifts the interval by m.
Русский
Пусть n ∈ ℕ и m ∈ ℕ, и i, j ∈ Fin(n). Образ открытого интервального множества uIoo(i, j) при отображении x ↦ x + m равен uIoo(i + m, j + m).
LaTeX
$$$\mathrm{Set.image}(\lambda x: \mathrm{Fin}(n). x + m, \mathrm{Set.uIoo}(i, j)) = \mathrm{Set.uIoo}(i.addNat m, j.addNat m)$$$
Lean4
@[simp]
theorem image_addNat_uIoo (m) (i j : Fin n) : (addNat · m) '' uIoo i j = uIoo (i.addNat m) (j.addNat m) := by
simp [uIoo, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]
