Theorems · Theorem · measure theory

MeasureTheory.VectorMeasure.of_biUnion_finset

∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {ι : Type u_4} {s : Finset ι} {f : ι → Set α},
  (↑s).PairwiseDisjoint f → (∀ b ∈ s, MeasurableSet (f b)) → v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p)

Defined in

Mathlib.MeasureTheory.VectorMeasure.Basic

Cited by

3 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpaceT2Space