insert_Ico_right_eq_Ico_add_one — Mathlib

English

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

Русский

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

LaTeX

$$$Ico(a,b) \cup \{b\} = 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

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