Ico_succ_right_eq_Icc

Mathlib.Order.Interval.Set.SuccPred

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

English

If there is no maximum, Ico a (succ b) equals Icc a b.

Русский

Если максимум не существует, Ico a (succ b) равно Icc a b.

LaTeX

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

Lean4

theorem Ico_succ_right_eq_Icc (a b : α) : Ico a (succ b) = Icc a b :=
  Ico_succ_right_eq_Icc_of_not_isMax (not_isMax _) _

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

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

Разделы

Аффилиация

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