Icc_pred_left

Mathlib.Order.SuccPred.Basic

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

← MathLib Explorer

English

If pred(a) ≤ b, then Icc(pred a, b) equals insert(pred a, Icc(a, b)).

Русский

Если pred(a) ≤ b, то Icc(pred(a), b) равно добавлению pred(a) в Icc(a, b).

LaTeX

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

Lean4

theorem Icc_pred_left (h : pred a ≤ b) : Icc (pred a) b = insert (pred a) (Icc a b) := by
  simp_rw [← Ici_inter_Iic, Ici_pred, insert_inter_of_mem (mem_Iic.2 h)]

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

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

Разделы

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

Аффилиация

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