map_castAddEmb_Ioi — Mathlib

English

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

Русский

При любом i и не нулевом m образ Ioi i под castAddEmb m равен Ioo (castAdd m i) (natAdd n 0).

LaTeX

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

Lean4

@[simp]
theorem map_castAddEmb_Ioi (m) [NeZero m] (i : Fin n) : (Ioi i).map (castAddEmb m) = Ioo (castAdd m i) (natAdd n 0) :=
  by simp [← coe_inj]

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