insert_Ioc_right_eq_Ioc_add_one — Mathlib

English

Similarly, adding the endpoint b+1 to the interval Ioc(a,b) yields Ioc(a,b+1): Ioc(a,b) ∪ {b+1} = Ioc(a,b+1).

Русский

Аналогично, добавление b+1 к интервалу Ioc(a,b) дает Ioc(a,b+1): Ioc(a,b) ∪ {b+1} = Ioc(a,b+1).

LaTeX

$$$ \mathrm{Ioc}(a,b) \cup \{b+1\} = \mathrm{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 _)

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