Ioo_succ_right_of_not_isMax — Mathlib

English

In a linear order with successor, if b is not maximal, then the open-closed interval Ioo(a, succ(b)) equals Ioc(a, b).

Русский

В линейном порядке с операцией следующего элемента, если b не максимален, то Ioo(a, succ(b)) = Ioc(a, b).

LaTeX

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

Lean4

theorem Ioo_succ_right_of_not_isMax (hb : ¬IsMax b) : Ioo a (succ b) = Ioc a b := by
  rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]

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