Ico_pred_left

Mathlib.Order.SuccPred.Basic

URI: https://scilib.ai/kg/mathlib#Order.Ico_pred_left

← MathLib Explorer

English

If pred(a) < b, then Ico(pred a, b) equals insert(pred a, Ico(a, b)).

Русский

Если pred(a) < b, тогда Ico(pred(a), b) = insert(pred(a), Ico(a, b)).

LaTeX

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

Lean4

theorem Ico_pred_left (h : pred a < b) : Ico (pred a) b = insert (pred a) (Ico a b) := by
  simp_rw [← Ici_inter_Iio, Ici_pred, insert_inter_of_mem (mem_Iio.2 h)]

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

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

Разделы

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

Аффилиация

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