Ioc_pred_left_eq_Icc

Mathlib.Order.Interval.Set.SuccPred

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

English

For any a,b, Ioc(pred(a), b) = Icc(a, b) when NoMinOrder holds, i.e., a is not necessarily min.

Русский

Для любых a,b, Ioc(pred(a), b) = Icc(a, b), если выполняется NoMinOrder.

LaTeX

$$$Ioc(\operatorname{pred} a, b) = \mathrm{Icc}(a, b)$$$

Lean4

theorem Ioc_pred_left_eq_Icc (a b : α) : Ioc (pred a) b = Icc a b :=
  Ioc_pred_left_eq_Icc_of_not_isMin (not_isMin _) _

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

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

Разделы

Аффилиация

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