Ico_succ_right_eq_Icc

Mathlib.Order.Interval.Finset.SuccPred

URI: https://scilib.ai/kg/mathlib#Finset.Ico_succ_right_eq_Icc

English

For any a,b with NoMaxOrder, Ico a (succ b) equals Icc a b.

Русский

Для любых a,b с NoMaxOrder: Ico a (succ b) = Icc a b.

LaTeX

$$$[NoMaxOrder\ α] \Rightarrow \mathrm{Ico}(a, \mathrm{succ}(b)) = \mathrm{Icc}(a,b)$$$

Lean4

theorem Ico_succ_right_eq_Icc (a b : α) : Ico a (succ b) = Icc a b :=
  coe_injective <| by simp

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

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

Разделы

Аффилиация

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