finsetImage_succ_Iic

Mathlib.Order.Interval.Finset.Fin

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

English

The image of Iic i under succ is Ioc 0 i.succ.

Русский

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

LaTeX

$$$ (Iic i).image succ = Ioc 0 i.succ $$$

Lean4

@[simp]
theorem finsetImage_succ_Iic (i : Fin n) : (Iic i).image succ = Ioc 0 i.succ := by simp [← coe_inj]

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

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

Разделы

Аффилиация

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