Ioo_succ_right_eq_Ioc_of_not_isMax

English

In a linearly ordered locally finite successor-order, if b is not maximal, then Ioo a (succ b) equals Ioc a b for all a.

Русский

В линейно упорядоченном локально конечном порядке с succ, если b не максимален, то Ioo a (succ b) = Ioc a b для всех a.

LaTeX

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

Lean4

theorem Ioo_succ_right_eq_Ioc_of_not_isMax (hb : ¬IsMax b) (a : α) : Ioo a (succ b) = Ioc a b :=
  coe_injective <| by simpa using Set.Ioo_succ_right_eq_Ioc_of_not_isMax hb _

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