sum_apply_of_countable — Mathlib

English

If the index set ι is countable, then for any family μ: ι → Measure α and any set S, the sum equals the infinite sum of the values: sum μ S = ∑' i, μ_i S.

Русский

Если индексный набор ι посчётен, то для любого множества S выполняется: сумма по индексу μ_i(S) равна сумме по i: sum μ S = ∑' i, μ_i S.

LaTeX

$$$ (\sum_i μ_i)(S) = \sum_i μ_i(S) \quad \text{при } [Countable ι] $$$

Lean4

theorem sum_apply_of_countable [Countable ι] (f : ι → Measure α) (s : Set α) : sum f s = ∑' i, f i s :=
  by
  apply le_antisymm ?_ (le_sum_apply _ _)
  rcases exists_measurable_superset_forall_eq f s with ⟨t, hst, htm, ht⟩
  calc
    sum f s ≤ sum f t := measure_mono hst
    _ = ∑' i, f i t := (sum_apply _ htm)
    _ = ∑' i, f i s := by simp [ht]

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