finsetImage_castAdd_Iic — Mathlib

English

For any Fin n and m, the image of Iic i under castAdd m equals Iic (castAdd m i).

Русский

Для любых i ∈ Fin n и m ∈ ℕ образ Iic i под castAdd m равен Iic (castAdd m i).

LaTeX

$$$ (\mathrm{Finset}.Iic\, i).image (\mathrm{Fin.castAdd}\, m) = \mathrm{Finset}.Iic\ (\mathrm{Fin.castAdd}\, m\, i) $$$

Lean4

@[simp]
theorem finsetImage_castAdd_Iic (m) (i : Fin n) : (Iic i).image (castAdd m) = Iic (castAdd m i) :=
  finsetImage_castLE_Iic i _

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