finsetImage_succ_Ioc

Mathlib.Order.Interval.Finset.Fin

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem finsetImage_succ_Ioc (i j : Fin n) : (Ioc i j).image succ = Ioc i.succ j.succ :=
  finsetImage_addNat_Ioc ..

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

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

Разделы

Аффилиация

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