map_castAddEmb_Icc — Mathlib

English

For any n, i, j, the image under the embed castAddEmb of the closed interval Icc i j is Icc (castAdd m i) (castAdd m j).

Русский

Для любых n, i, j образ Icc i j под отображением castAddEmb равен Icc (castAdd m i) (castAdd m j).

LaTeX

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

Lean4

@[simp]
theorem map_castAddEmb_Icc (m) (i j : Fin n) : (Icc i j).map (castAddEmb m) = Icc (castAdd m i) (castAdd m j) :=
  map_castLEEmb_Icc ..

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