Theorems · Theorem · measure theory

MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : AddCommMonoid β]
  (T : Set α → β),
  T ∅ = 0 →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ {ι : Type u_8} (S : ι → Set α) (sι : Finset ι),
        (∀ (i : ι), MeasurableSet (S i)) →
          (∀ i ∈ sι, μ (S i) ≠ ⊤) →
            (∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)) → T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)

Defined in

Mathlib.MeasureTheory.Integral.FinMeasAdditive

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoid