Icc_succ_left_eq_Ioc

Mathlib.Order.Interval.Set.SuccPred

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

English

For any a,b with NoMaxOrder, Icc(succ a) b = Ioc(a,b).

Русский

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

LaTeX

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

Lean4

theorem Icc_succ_left_eq_Ioc (a b : α) : Icc (succ a) b = Ioc a b :=
  Icc_succ_left_eq_Ioc_of_not_isMax (not_isMax _) _

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

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

Разделы

Аффилиация

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