image_castAdd_Iio

Mathlib.Order.Interval.Set.Fin

URI: https://scilib.ai/kg/mathlib#Fin.image_castAdd_Iio

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_castAdd_Iio (m) (i : Fin n) : castAdd m '' Iio i = Iio (castAdd m i) :=
  image_castLE_Iio ..

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru