insert_Icc_left_eq_Icc_sub_one

Mathlib.Algebra.Order.Interval.Set.SuccPred

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

← MathLib Explorer

English

If h: a-1 ≤ b, then insert a-1 into Icc a b equals Icc(a-1) b: insert (a-1) (Icc a b) = Icc(a-1, b).

Русский

Пусть a-1 ≤ b. Тогда вставка a-1 в Icc a b дает Icc(a-1, b).

LaTeX

$$$(a-1) \text{ вставка } Icc(a,b) = Icc(a-1,b)$$$

Lean4

theorem insert_Icc_left_eq_Icc_sub_one (h : a - 1 ≤ b) : insert (a - 1) (Icc a b) = Icc (a - 1) b := by
  simpa [← pred_eq_sub_one] using insert_Icc_left_eq_Icc_pred (pred_eq_sub_one a ▸ h)

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

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

Разделы

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

Аффилиация

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