image_natAdd_Ici — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_natAdd_Ici (m) (i : Fin n) : natAdd m '' Ici i = Ici (natAdd m i) :=
  by
  rw [← preimage_natAdd_Ici_natAdd, image_preimage_eq_of_subset]
  rw [range_natAdd]
  exact fun j hj ↦ Nat.le_trans (le_coe_natAdd ..) hj

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