insert_Ico_sub_one_right_eq_Ico

Mathlib.Algebra.Order.Interval.Set.SuccPred

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

← MathLib Explorer

English

For a < b, inserting b-1 into Ico(a, b-1) yields Ico(a, b): Ico(a, b-1) ∪ {b-1} = Ico(a, b).

Русский

При a < b вставка b-1 в Ico(a, b-1) даёт Ico(a, b).

LaTeX

$$$Ico(a,b-1) \cup \{b-1\} = Ico(a,b)$$$

Lean4

theorem insert_Ico_sub_one_right_eq_Ico (h : a < b) : insert (b - 1) (Ico a (b - 1)) = Ico a b := by
  simpa [pred_eq_sub_one] using insert_Ico_pred_right_eq_Ico h

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

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

Разделы

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

Аффилиация

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