insert_Ioc_right_eq_Ioc_add_one — Mathlib

English

If a ≤ b, then inserting b+1 into the open-closed interval Ioc(a, b) yields Ioc(a, b+1): Ioc(a,b) ∪ {b+1} = Ioc(a,b+1).

Русский

Если a ≤ b, то добавление b+1 к открытому слева, закрытому справа интервалу Ioc(a,b) даёт Ioc(a,b+1).

LaTeX

$$$Ioc(a,b) \cup \{b+1\} = Ioc(a,b+1)$$$

Lean4

theorem insert_Ioc_right_eq_Ioc_add_one (h : a ≤ b) : insert (b + 1) (Ioc a b) = Ioc a (b + 1) :=
  insert_Ioc_right_eq_Ioc_add_one_of_not_isMax h (not_isMax _)

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