image_addNat_uIcc — Mathlib

English

For all m ∈ ℕ and i, j ∈ Fin(n), the image of uIcc(i, j) under x ↦ x + m is uIcc(i + m, j + m).

Русский

Для всех m ∈ ℕ и i, j ∈ Fin(n) образ uIcc(i, j) при сдвиге на m равен uIcc(i + m, j + m).

LaTeX

$$$$ \\mathrm{Set.image}(\\\\mathrm{Fin.natAdd}(m))(\\\\mathrm{Set.uIcc}(i,j)) = \\\\mathrm{Set.uIcc}(\\\\mathrm{Fin.natAdd}(m)i, \\\\mathrm{Fin.natAdd}(m)j). $$$$

Lean4

@[simp]
theorem image_addNat_uIcc (m) (i j : Fin n) : (addNat · m) '' uIcc i j = uIcc (i.addNat m) (j.addNat m) := by
  simp [uIcc, ← (strictMono_addNat m).monotone.map_max, ← (strictMono_addNat m).monotone.map_min]

Похожие утверждения