image_addNat_Ici — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\mathrm{Set.image}(\\\\mathrm{Fin.natAdd}(m))(\\\\mathrm{Set.Ici} i) = \\\\mathrm{Set.Ici}(\\\\mathrm{Fin.natAdd}(m)i). $$$$

Lean4

@[simp]
theorem image_addNat_Ici (m) (i : Fin n) : (addNat · m) '' Ici i = Ici (i.addNat m) :=
  by
  rw [← preimage_addNat_Ici_addNat, image_preimage_eq_of_subset]
  intro j hj
  have : (i : ℕ) + m ≤ j := hj
  refine ⟨⟨j - m, by cutsat⟩, ?_⟩
  simp (disch := omega)

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