map_castAddEmb_Ici — Mathlib

English

For any Fin n and NeZero m, the image of Ici i under castAddEmb m equals Ico (castAdd m i) (natAdd n 0).

Русский

Для любого i и не нулевого m образ Ici i под castAddEmb m равен Ico (castAdd m i) (natAdd n 0).

LaTeX

$$$ (\mathrm{Fin}.Ici\, i).image (\mathrm{Fin.castAddEmb}\, m) = \mathrm{Finset}.Ico\ (\mathrm{Fin.castAdd}\, m\, i) (\mathrm{Fin.natAdd}\, n\, 0) $$$

Lean4

@[simp]
theorem map_castAddEmb_Ici (m) [NeZero m] (i : Fin n) : (Ici i).map (castAddEmb m) = Ico (castAdd m i) (natAdd n 0) :=
  by simp [map_eq_image]

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