image_natAdd_Icc — Mathlib

English

The image of Icc(i, j) under natAdd m is Icc(natAdd m i, natAdd m j).

Русский

Образ Icc(i, j) под natAdd m равен Icc(natAdd m i, natAdd m j).

LaTeX

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

Lean4

@[simp]
theorem image_natAdd_Icc (m) (i j : Fin n) : natAdd m '' Icc i j = Icc (natAdd m i) (natAdd m j) :=
  by
  rw [← preimage_natAdd_Icc_natAdd, image_preimage_eq_of_subset]
  exact Icc_subset_Ici_self.trans <| image_natAdd_Ici m i ▸ image_subset_range _ _

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