insert_Icc_add_one_left_eq_Icc

Mathlib.Algebra.Order.Interval.Set.SuccPred

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

← MathLib Explorer

English

Translation by a maps Ioi b to Ioi(b + a).

Русский

Сдвиг на a отображает Ioi b в Ioi(b + a).

LaTeX

$$$Ioi(b,c) + a = Ioi(b+a,c+a)$$$

Lean4

theorem insert_Icc_add_one_left_eq_Icc (h : a ≤ b) : insert a (Icc (a + 1) b) = Icc a b := by
  simpa [succ_eq_add_one] using insert_Icc_succ_left_eq_Icc h

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

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

Разделы

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

Аффилиация

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