insert_Ico_right_eq_Ico_add_one — Mathlib

English

In the discrete order, adding the endpoint b to the half-open interval Ico(a,b) yields Ico(a,b+1): Ico(a,b) ∪ {b} = Ico(a,b+1).

Русский

При дискретном порядке добавление концевого элемента b к полузакрытому интервалу Ico(a,b) дает Ico(a,b+1): Ico(a,b) ∪ {b} = Ico(a,b+1).

LaTeX

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

Lean4

theorem insert_Ico_right_eq_Ico_add_one (h : a ≤ b) : insert b (Ico a b) = Ico a (b + 1) := by
  simpa [succ_eq_add_one] using insert_Ico_right_eq_Ico_succ h

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