addContent_accumulate — Mathlib

English

Let s(i) ∈ C be a sequence of sets. Then m(Set.Accumulate s n) equals the sum of the first n+1 terms: ∑_{i=0}^n m(s(i)).

Русский

Для последовательности множеств s(i) ∈ C верно m(Accumulate s n) = ∑_{i=0}^n m(s(i)).

LaTeX

$$m(\mathrm{Accumulate}(s,n)) = \sum_{i=0}^{n} m(s(i))$$

Lean4

theorem addContent_accumulate (m : AddContent C) (hC : IsSetRing C) {s : ℕ → Set α} (hs_disj : Pairwise (Disjoint on s))
    (hsC : ∀ i, s i ∈ C) (n : ℕ) : m (Set.Accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i) := by
  induction n with
  | zero => simp
  | succ n hn =>
    rw [Finset.sum_range_succ, ← hn, Set.accumulate_succ, addContent_union hC _ (hsC _)]
    · exact Set.disjoint_accumulate hs_disj (Nat.lt_succ_self n)
    · exact hC.accumulate_mem hsC n

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