Theorem MeasureTheory.IsSetSemiring.isSetRing_supClosure

Modification history

2026-01-27 11:49
Mathlib/MeasureTheory/SetSemiring.lean
feat(MeasureTheory): the `supClosure` of a semiring of sets is a ring (#34470)
Added MeasureTheory.IsSetSemiring.isSetRing_supClosureView on Github →