Commit 2024-08-15 14:22 6ac635f5

View on Github →

feat: Add partialSups lemmas (#15291)

Estimated changes

Modified Mathlib/MeasureTheory/SetSemiring.lean

added theorem MeasureTheory.IsSetRing.disjointed_mem

added theorem MeasureTheory.IsSetRing.partialSups_mem

Modified Mathlib/Order/PartialSups.lean

modified theorem partialSups_eq_biSup

added theorem partialSups_eq_biUnion_range

added theorem partialSups_eq_sUnion_image

added theorem partialSups_monotone