Ioo_succ_right

Mathlib.Order.SuccPred.Basic

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

English

If a ≤ b and b is not maximal, then Ioo(a, succ(b)) equals insert b Ioo(a,b).

Русский

Если a ≤ b и b не максимален, то Ioo(a, succ(b)) = insert b Ioo(a,b).

LaTeX

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

Lean4

@[simp]
theorem Ioo_succ_right (a b : α) : Ioo a (succ b) = Ioc a b :=
  Ioo_succ_right_of_not_isMax <| not_isMax _

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

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

Разделы

Аффилиация

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