image_natAdd_Ioi — Mathlib

English

The image of Ioi i under natAdd m is Ioi (natAdd m i).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_natAdd_Ioi (m) (i : Fin n) : natAdd m '' Ioi i = Ioi (natAdd m i) :=
  by
  rw [← preimage_natAdd_Ioi_natAdd, image_preimage_eq_of_subset]
  exact Ioi_subset_Ici_self.trans <| image_natAdd_Ici m i ▸ image_subset_range _ _

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