map_castAddEmb_Ioc — Mathlib

English

The image of Ioc i j under castAddEmb m is Ioc (castAdd m i) (castAdd m j).

Русский

Образ Ioc i j под castAddEmb m равен Ioc (castAdd m i) (castAdd m j).

LaTeX

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

Lean4

@[simp]
theorem map_castAddEmb_Ioc (m) (i j : Fin n) : (Ioc i j).map (castAddEmb m) = Ioc (castAdd m i) (castAdd m j) :=
  map_castLEEmb_Ioc ..

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