Ico_succ_succ_eq_Ioc

Mathlib.Order.Interval.Set.SuccPred

URI: https://scilib.ai/kg/mathlib#Set.Ico_succ_succ_eq_Ioc

English

For any a,b, Ico(succ a) (succ b) equals Ioc a b.

Русский

Для любых a,b: Ico(succ a) (succ b) равна Ioc a b.

LaTeX

$$$\\mathrm{Ico}(\\mathrm{Order.succ}\\,a, \\mathrm{Order.succ}\\,b) = \\mathrm{Ioc}(a,b)$$$

Lean4

theorem Ico_succ_succ_eq_Ioc (a b : α) : Ico (succ a) (succ b) = Ioc a b :=
  Ico_succ_succ_eq_Ioc_of_not_isMax (not_isMax _) _

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

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

Разделы

Аффилиация

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