Ioo_succ_right_eq_Ioc

Mathlib.Order.Interval.Finset.SuccPred

URI: https://scilib.ai/kg/mathlib#Finset.Ioo_succ_right_eq_Ioc

English

For NoMaxOrder, Ioo a (succ b) equals Ioc a b.

Русский

При NoMaxOrder: Ioo a (succ b) = Ioc a b.

LaTeX

$$$[NoMaxOrder\ α] \Rightarrow \mathrm{Ioo}(a, \mathrm{succ}(b)) = \mathrm{Ioc}(a,b)$$$

Lean4

theorem Ioo_succ_right_eq_Ioc (a b : α) : Ioo a (succ b) = Ioc a b :=
  coe_injective <| by simp

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

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

Разделы

Аффилиация

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