Ico_add_Ico_eq_Ico — Mathlib

English

If a ≤ b ≤ c, then the multiset sum of Ico(a,b) and Ico(b,c) equals Ico(a,c).

Русский

Если a ≤ b ≤ c, то сумма по компонентам множеств Ico(a,b) и Ico(b,c) равна Ico(a,c).

LaTeX

$$$ a \le b \land b \le c \Rightarrow Ico(a,b) + Ico(b,c) = Ico(a,c) $$$

Lean4

theorem Ico_add_Ico_eq_Ico {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) : Ico a b + Ico b c = Ico a c := by
  rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]

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