map_castAddEmb_Ico — Mathlib

English

The image of Ico i j under the embedding castAddEmb m is Ico (castAdd m i) (castAdd m j).

Русский

Образ Ico i j под встраиванием castAddEmb m равен Ico (castAdd m i) (castAdd m j).

LaTeX

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

Lean4

@[simp]
theorem map_castAddEmb_Ico (m) (i j : Fin n) : (Ico i j).map (castAddEmb m) = Ico (castAdd m i) (castAdd m j) :=
  map_castLEEmb_Ico ..

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