insert_Ioc_pred_right_eq_Ioc

Mathlib.Order.Interval.Set.SuccPred

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

← MathLib Explorer

English

If a < b, inserting pred(b) into Ioc(a, pred(b)) yields Ioc(a, b).

Русский

Если a < b, вставка pred(b) в Ioc(a, pred(b)) дает Ioc(a, b).

LaTeX

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

Lean4

theorem insert_Ioc_pred_right_eq_Ioc (h : a < b) : insert b (Ioc a (pred b)) = Ioc a b := by
  rw [Ioc_pred_right_of_not_isMin h.not_isMin, Ioo_insert_right h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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