Commit 2026-01-26 08:43 83c98ba4

View on Github →

feat: let AddContent take values in a general monoid (#34434) Needed to construct vector measures in #34055. The PR only changes the definition and fixes things (notably by moving things around wrt variable lines). No lemma added or removed.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

modified def MeasureTheory.AddContent.IsSigmaSubadditive

modified def MeasureTheory.AddContent.extend

modified def MeasureTheory.IsSetRing.addContent_of_union

modified theorem MeasureTheory.addContent_accumulate

modified theorem MeasureTheory.addContent_diff_of_ne_top

modified theorem MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero

modified theorem MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive

modified theorem MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le

modified theorem MeasureTheory.addContent_le_sum_of_subset_sUnion

modified theorem MeasureTheory.addContent_sUnion_le_sum

modified theorem MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum

modified theorem MeasureTheory.le_addContent_diff

modified theorem MeasureTheory.tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum

Modified Mathlib/MeasureTheory/OuterMeasure/OfAddContent.lean

modified theorem MeasureTheory.AddContent.inducedOuterMeasure_eq

modified theorem MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure

modified theorem MeasureTheory.AddContent.isCaratheodory_inducedOuterMeasure_of_mem

modified theorem MeasureTheory.AddContent.isCaratheodory_ofFunction_of_mem

modified theorem MeasureTheory.AddContent.measureCaratheodory_eq

modified theorem MeasureTheory.AddContent.measureCaratheodory_eq_inducedOuterMeasure

modified theorem MeasureTheory.AddContent.measure_eq

modified theorem MeasureTheory.AddContent.ofFunction_eq

Modified Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean

Modified Mathlib/Probability/ProductMeasure.lean