insert_Ico_right_eq_Ico_add_one_of_not_isMax

English

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

Русский

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

LaTeX

$$$a \le b \land \neg \mathrm{IsMax}(b) \Rightarrow \operatorname{insert}(b, Ico(a,b)) = Ico(a,b+1)$$$

Lean4

theorem insert_Ico_right_eq_Ico_add_one_of_not_isMax (h : a ≤ b) (hb : ¬IsMax b) : insert b (Ico a b) = Ico a (b + 1) :=
  by simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ_of_not_isMax h hb

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