Commit 2025-01-29 21:38 3ba0a028

View on Github →

feat(MeasureTheory/SetSemiring.lean, Order/CompleteLattice.lean): change SetSemiring allow writing unions as disjoint unions (#20931) We show that a union of sets in a semiring can be written as the disjoint unions of sets in the semiring, and add several lemmas. First PR in a work towards the Caratheodory extension theorem, when starting with a SetSemiring.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/AddContent.lean

deleted theorem MeasureTheory.addContent_eq_add_diffFinset₀_of_subset

added theorem MeasureTheory.addContent_eq_add_disjointOfDiffUnion_of_subset

Modified Mathlib/MeasureTheory/SetSemiring.lean

deleted theorem MeasureTheory.IsSetSemiring.diffFinset_subset

deleted theorem MeasureTheory.IsSetSemiring.diffFinset₀_subset

deleted theorem MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_diffFinset₀

added theorem MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion

added theorem MeasureTheory.IsSetSemiring.disjointOfDiffUnion_subset

added theorem MeasureTheory.IsSetSemiring.disjointOfUnion_props

added theorem MeasureTheory.IsSetSemiring.disjointOfUnion_subset

added theorem MeasureTheory.IsSetSemiring.disjointOfUnion_subset_of_mem

deleted theorem MeasureTheory.IsSetSemiring.disjoint_diffFinset₀

added theorem MeasureTheory.IsSetSemiring.disjoint_disjointOfDiffUnion

deleted theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_diffFinset

deleted theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_diffFinset₀

added theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff

added theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion

added theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfDiff

added theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfDiffUnion

added theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfUnion

deleted theorem MeasureTheory.IsSetSemiring.empty_not_mem_diffFinset

deleted theorem MeasureTheory.IsSetSemiring.empty_not_mem_diffFinset₀

added theorem MeasureTheory.IsSetSemiring.nmem_disjointOfDiff

deleted theorem MeasureTheory.IsSetSemiring.not_mem_diffFinset

added theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion

deleted theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_diffFinset

deleted theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_diffFinset₀

added theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff

added theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion

added theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion

added theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem

deleted theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_diffFinset

added theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff

deleted theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_diffFinset₀

added theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion

deleted theorem MeasureTheory.IsSetSemiring.sUnion_diffFinset

deleted theorem MeasureTheory.IsSetSemiring.sUnion_diffFinset₀_subset

added theorem MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff

added theorem MeasureTheory.IsSetSemiring.sUnion_disjointOfDiffUnion_subset

added theorem MeasureTheory.IsSetSemiring.sUnion_disjointOfUnion

deleted theorem MeasureTheory.IsSetSemiring.sUnion_insert_diffFinset

added theorem MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff

deleted theorem MeasureTheory.IsSetSemiring.sUnion_union_diffFinset₀_of_subset

added theorem MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset

deleted theorem MeasureTheory.IsSetSemiring.sUnion_union_sUnion_diffFinset₀_of_subset

added theorem MeasureTheory.IsSetSemiring.sUnion_union_sUnion_disjointOfDiffUnion_of_subset

added theorem MeasureTheory.IsSetSemiring.subset_disjointOfDiff

added theorem MeasureTheory.IsSetSemiring.subset_of_diffUnion_disjointOfDiffUnion

added theorem MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfDiffUnion

added theorem MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfUnion

Modified Mathlib/Order/CompleteLattice.lean

added theorem disjoint_of_sSup_disjoint

added theorem disjoint_of_sSup_disjoint_of_le_of_le