image_natAdd_uIoc — Mathlib

English

Let m ∈ ℕ and i, j ∈ Fin(n). The image of uIoc(i, j) under x ↦ x + m is uIoc(i + m, j + m).

Русский

Пусть m ∈ ℕ и i, j ∈ Fin(n). Образ uIoc(i, j) при сдвиге на m равен uIoc(i + m, j + m).

LaTeX

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

Lean4

@[simp]
theorem image_natAdd_uIoc (m) (i j : Fin n) : natAdd m '' uIoc i j = uIoc (natAdd m i) (natAdd m j) := by
  simp [uIoc, ← (strictMono_natAdd m).monotone.map_max, ← (strictMono_natAdd m).monotone.map_min]

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