finsetImage_succ_Ioo

Mathlib.Order.Interval.Finset.Fin

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

English

The image of Ioo i j under succ is Ioo i.succ j.succ.

Русский

Образ Ioo i j под succ равен Ioo i.succ j.succ.

LaTeX

$$$ (Ioo i j).image succ = Ioo i.succ j.succ $$$

Lean4

@[simp]
theorem finsetImage_succ_Ioo (i j : Fin n) : (Ioo i j).image succ = Ioo i.succ j.succ :=
  finsetImage_addNat_Ioo ..

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

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

Разделы

Аффилиация

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