measure_biUnion_finset — Mathlib

English

Let s be a Finite index set and f: s → Set α. If every f(b) is measurable for b ∈ s, then μ(⋃ b ∈ s, f(b)) = ∑ p ∈ s μ(f(p)).

Русский

Пусть s — конечное множество индексов и для каждого b ∈ s множество f(b) измеримо. Тогда μ(⋃_{b∈s} f(b)) = ∑_{b∈s} μ(f(b)).

LaTeX

$$$$ \\mu\\left(\\bigcup_{b \\in s} f(b)\\right) = \\sum_{p \\\\in s} \\mu\\left(f(p)\\right). $$$$

Lean4

theorem measure_biUnion_finset {s : Finset ι} {f : ι → Set α} (hd : PairwiseDisjoint (↑s) f)
    (hm : ∀ b ∈ s, MeasurableSet (f b)) : μ (⋃ b ∈ s, f b) = ∑ p ∈ s, μ (f p) :=
  measure_biUnion_finset₀ hd.aedisjoint fun b hb => (hm b hb).nullMeasurableSet

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