image_castAdd_Iic

Mathlib.Order.Interval.Set.Fin

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem image_castAdd_Iic (m) (i : Fin n) : castAdd m '' Iic i = Iic (castAdd m i) :=
  image_castLE_Iic i _

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

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

Разделы

Аффилиация

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