Ioc_pred_left_eq_Icc

Mathlib.Order.Interval.Finset.SuccPred

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

English

With a, b in a linearly ordered set and NoMinOrder, the left-closed-right-closed interval after pred(a) equals the closed interval [a, b].

Русский

Пусть a и b в линейном порядке, NoMinOrder. Тогда Ioc(pred(a), b) = Icc(a, b).

LaTeX

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

Lean4

theorem Ioc_pred_left_eq_Icc (a b : α) : Ioc (pred a) b = Icc a b :=
  coe_injective <| by simp

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

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

Разделы

Аффилиация

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