Theorems · Theorem · measure theory

MeasureTheory.AddContent.supClosure_apply_finpartition

∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent G C) {s : Set α} {J : Finpartition s},
  ↑J.parts ⊆ C → (m.supClosure hC) s = ∑ s ∈ J.parts, m s

Defined in

Mathlib.MeasureTheory.Measure.AddContent

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoid