Ico_succ_right_eq_Icc_of_not_isMax

English

In a linearly ordered locally finite successor-order, if b is not maximal, then Ico a (succ b) = Icc a b for all a.

Русский

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

LaTeX

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

Lean4

theorem Ico_succ_right_eq_Icc_of_not_isMax (hb : ¬IsMax b) (a : α) : Ico a (succ b) = Icc a b :=
  coe_injective <| by simpa using Set.Ico_succ_right_eq_Icc_of_not_isMax hb _

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