Commit 2024-01-18 15:51 6cdea122

View on Github →

feat(MeasureTheory): define contents on semi-rings of sets (#9402)

Define additive contents and prove their basic properties on (semi)-rings of sets.
Define rings of sets. Part of the formalization of the Kolmogorov Extension Theorem.

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Measure/AddContent.lean

added structure MeasureTheory.AddContent

added theorem MeasureTheory.addContent_biUnion_le

added theorem MeasureTheory.addContent_empty

added theorem MeasureTheory.addContent_eq_add_diffFinset₀_of_subset

added theorem MeasureTheory.addContent_mono

added theorem MeasureTheory.addContent_sUnion

added theorem MeasureTheory.addContent_union'

added theorem MeasureTheory.addContent_union

added theorem MeasureTheory.addContent_union_le

added theorem MeasureTheory.le_addContent_diff

added theorem MeasureTheory.sum_addContent_le_of_subset

Modified Mathlib/MeasureTheory/SetSemiring.lean

added theorem MeasureTheory.IsSetRing.biInter_mem

added theorem MeasureTheory.IsSetRing.biUnion_mem

added theorem MeasureTheory.IsSetRing.inter_mem

added theorem MeasureTheory.IsSetRing.isSetSemiring

added structure MeasureTheory.IsSetRing