insert_Ico_right_eq_Ico_succ_of_not_isMax

English

If a ≤ b and b is not maximal, then inserting b into Ico a b yields Ico a (succ b).

Русский

Если a ≤ b и b не максимален, вставка b в Ico a b даёт Ico a (succ b).

LaTeX

$$$\\text{insert } b (\\text{Ico } a b) = \\text{Ico } a (\\mathrm{Order.succ}\\,b)$ under not isMax(b).$$

Lean4

theorem insert_Ico_right_eq_Ico_succ_of_not_isMax (h : a ≤ b) (hb : ¬IsMax b) : insert b (Ico a b) = Ico a (succ b) :=
  by rw [Ico_succ_right_of_not_isMax hb, ← Ico_insert_right h]

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