finsetImage_castAdd_Icc — Mathlib

English

For any Fin n and m, the image of the closed interval Icc i j under the addition-cast map castAdd m is the closed interval between castAdd m i and castAdd m j.

Русский

Для любых i, j ∈ Fin n и m ∈ ℕ образ изображения замкнутого интервала Icc i j под отображением castAdd m равен замкнутому интервалу между castAdd m i и castAdd m j.

LaTeX

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

Lean4

@[simp]
theorem finsetImage_castAdd_Icc (m) (i j : Fin n) : (Icc i j).image (castAdd m) = Icc (castAdd m i) (castAdd m j) :=
  finsetImage_castLE_Icc ..

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