Commit 2026-01-27 11:49 4013362a

View on Github →

feat(MeasureTheory): the supClosure of a semiring of sets is a ring (#34470)

Estimated changes

Modified Mathlib/MeasureTheory/SetSemiring.lean

added theorem MeasureTheory.IsSetSemiring.diff_mem_supClosure

added theorem MeasureTheory.IsSetSemiring.exists_finpartition_diff

added theorem MeasureTheory.IsSetSemiring.isSetRing_supClosure

added theorem MeasureTheory.IsSetSemiring.mem_supClosure_iff