image_castAdd_uIcc — Mathlib

English

The image of uIcc i j under Fin.castAdd m is uIcc (castAdd m i) (castAdd m j).

Русский

Изображение uIcc i j под Fin.castAdd m равно uIcc (castAdd m i) (castAdd m j).

LaTeX

$$$$\\mathrm{Fin.castAdd}\\, m'' \\mathrm{uIcc} i j = \\mathrm{uIcc}(\\mathrm{Fin.castAdd}\\, m\\, i)(\\mathrm{Fin.castAdd}\\, m\\, j).$$$$

Lean4

@[simp]
theorem image_castAdd_uIcc (m) (i j : Fin n) : castAdd m '' uIcc i j = uIcc (castAdd m i) (castAdd m j) :=
  image_castLE_uIcc ..

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