restrict_biUnion — Mathlib

English

If T is a Finset of indices and s_i are measurable, then μ.restrict (⋃ i ∈ T, s_i) = sum_{i ∈ T} μ.restrict (s_i).

Русский

Пусть T — конечное множество индексов, и все s_i измеримы. Тогда ограничение объединения равно сумме ограничений по каждому s_i.

LaTeX

$$$\\mu\\restrict (\\bigcup_{i\\in T} s_i) = \\sum_{i\\in T} (\\mu\\restrict (s_i))$.$$

Lean4

theorem restrict_biUnion {s : ι → Set α} {T : Set ι} (hT : Countable T) (hd : T.Pairwise (Disjoint on s))
    (hm : ∀ i, MeasurableSet (s i)) : μ.restrict (⋃ i ∈ T, s i) = sum fun (i : T) => μ.restrict (s i) :=
  by
  rw [Set.biUnion_eq_iUnion]
  exact restrict_iUnion (fun i j hij ↦ hd i.coe_prop j.coe_prop (Subtype.coe_ne_coe.mpr hij)) (hm ·)

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