Theorems · Definition · measure theory

MeasureTheory.AddContent.supClosure

{α : Type u_1} →
  {C : Set (Set α)} →
    {G : Type u_2} →
      [inst : AddCommMonoid G] →
        MeasureTheory.AddContent G C → MeasureTheory.IsSetSemiring C → MeasureTheory.AddContent G (supClosure C)

Extend a content over C to the finite unions of elements of C by additivity.

Defined in: Mathlib.MeasureTheory.Measure.AddContent
Cited by: 5 results in Mathlib
Foundations: Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: AddCommMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Setstatement and proof · cited by 53,352
AddCommMonoidstatement and proof · cited by 12,281
ClosureOperatorstatement · cited by 371
MeasureTheory.IsSetSemiringstatement and proof · cited by 78
MeasureTheory.AddContentstatement and proof · cited by 78
supClosurestatement · cited by 33

Cited by5

Results whose statement or proof uses this declaration.

MeasureTheory.AddContent.supClosure_apply_of_memstatement · cited by 2
MeasureTheory.AddContent.supClosure_applystatement · cited by 1
MeasureTheory.AddContent.supClosure_apply_finpartitionstatement · cited by 1
MeasureTheory.addContent_le_sum_of_subset_sUnionproof · cited by 1
MeasureTheory.VectorMeasure.exists_extension_of_isSetSemiring_of_le_measure_of_denseproof · cited by 0