restrict_sum_of_countable — Mathlib

English

If ι is countable and μ is a family of measures, then restricting the sum over ι to a set s equals the sum of restricted measures: (sum μ).restrict s = sum_i (μ_i.restrict s).

Русский

Если ι счётно, то ограничение суммы по множеству s равно сумме ограничений по каждому μ_i.

LaTeX

$$$\\bigl(\\sum_i μ_i\\bigr)\\restrict s = \\sum_i (μ_i\\restrict s)$ for countable index set.$$

Lean4

@[simp]
theorem restrict_sum_of_countable [Countable ι] (μ : ι → Measure α) (s : Set α) :
    (sum μ).restrict s = sum fun i => (μ i).restrict s :=
  by
  ext t ht
  simp_rw [sum_apply _ ht, restrict_apply ht, sum_apply_of_countable]

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