sum_apply — Mathlib

English

Let (μ_i) be a family of measures on a space X. Then, for every measurable set S, the sum measure evaluated at S equals the sum of the individual measures: (∑ μ_i)(S) = ∑ μ_i(S).

Русский

Пусть (μ_i) — семейство мер на пространстве X. Тогда для каждого измеримого множества S выполняется: (∑ μ_i)(S) = ∑ μ_i(S).

LaTeX

$$$ (\sum_i μ_i)(S) = \sum_i μ_i(S) $$$

Lean4

@[simp]
theorem sum_apply (f : ι → Measure α) {s : Set α} (hs : MeasurableSet s) : sum f s = ∑' i, f i s :=
  toMeasure_apply _ _ hs

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