insert_Ioc_left_eq_Ioc_pred

Mathlib.Order.Interval.Set.SuccPred

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

English

If h: a ≤ b, then inserting a into Ioc(a, b) yields Ioc(pred a, b).

Русский

Пусть h: a ≤ b. Вставка a в Ioc(a, b) дает Ioc(pred a, b).

LaTeX

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

Lean4

theorem insert_Ioc_left_eq_Ioc_pred (h : a ≤ b) : insert a (Ioc a b) = Ioc (pred a) b :=
  insert_Ioc_left_eq_Ioc_pred_of_not_isMin h (not_isMin _)

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

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

Разделы

Аффилиация

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