restrict_sum — Mathlib

English

Let μ be a sum of measures μ = ∑ μ_i over an index set. For any measurable set s, the restriction distributes over the sum: (sum μ).restrict s = sum (μ_i.restrict s).

Русский

Пусть μ = ∑_i μ_i. Тогда для любого измеримого множества s выполнено: (sum μ).Restrict s = sum (μ_i.Restrict s).

LaTeX

$$$\\bigl(\\sum_i μ_i\\bigr)\\restrict s = \\sum_i (μ_i\\restrict s)$ for measurable $s$.$$

Lean4

@[simp]
theorem restrict_sum (μ : ι → Measure α) {s : Set α} (hs : MeasurableSet s) :
    (sum μ).restrict s = sum fun i => (μ i).restrict s :=
  ext fun t ht => by simp only [sum_apply, restrict_apply, ht, ht.inter hs]

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