Ico_succ_right_eq_insert

Mathlib.Order.SuccPred.Basic

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

English

If a ≤ b, then Ico(a, succ(b)) equals insert b Ico(a,b).

Русский

Если a ≤ b, то Ico(a, succ(b)) = insert b Ico(a,b).

LaTeX

$$$(a \le b) \Rightarrow \mathrm{Ico}(a, \operatorname{succ} b) = \operatorname{insert}(b)(\mathrm{Ico}(a, b))$$$

Lean4

theorem Ico_succ_right_eq_insert (h : a ≤ b) : Ico a (succ b) = insert b (Ico a b) :=
  Ico_succ_right_eq_insert_of_not_isMax h <| not_isMax b

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

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

Разделы

Аффилиация

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