# Semirings and rings of sets #

A semi-ring of sets `C` (in the sense of measure theory) is a family of sets containing `∅`, stable by intersection and such that for all `s, t ∈ C`, `t \ s` is equal to a disjoint union of finitely many sets in `C`. Note that a semi-ring of sets may not contain unions.

An important example of a semi-ring of sets is intervals in `ℝ`. The intersection of two intervals is an interval (possibly empty). The union of two intervals may not be an interval. The set difference of two intervals may not be an interval, but it will be a disjoint union of two intervals.

A ring of sets is a set of sets containing `∅`, stable by union, set difference and intersection.

## Main definitions #

- `MeasureTheory.IsSetSemiring C`: property of being a semi-ring of sets.

- `MeasureTheory.IsSetSemiring.disjointOfDiff hs ht`: for `s, t` in a semi-ring `C` (with `hC : IsSetSemiring C`) with `hs : s ∈ C`, `ht : t ∈ C`, this is a `Finset` of pairwise disjoint sets such that `s \ t = ⋃₀ hC.disjointOfDiff hs ht`.

- `MeasureTheory.IsSetSemiring.disjointOfDiffUnion hs hI`: for `hs : s ∈ C` and a finset `I` of sets in `C` (with `hI : ↑I ⊆ C`), this is a `Finset` of pairwise disjoint sets such that `s \ ⋃₀ I = ⋃₀ hC.disjointOfDiffUnion hs hI`.

- `MeasureTheory.IsSetSemiring.disjointOfUnion hJ`: for `hJ ⊆ C`, this is a `Finset` of pairwise disjoint sets such that `⋃₀ J = ⋃₀ hC.disjointOfUnion hJ`.

- `MeasureTheory.IsSetRing`: property of being a ring of sets.

## Main statements #

- `MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq`: the existence of the `Finset` given by the definition `IsSetSemiring.disjointOfDiffUnion` (see above).
- `MeasureTheory.IsSetSemiring.disjointOfUnion_props`: In a `hC : IsSetSemiring C`, for a `J : Finset (Set α)` with `J ⊆ C`, there is for every `x in J` some `K x ⊆ C` finite, such that
  - `⋃ x ∈ J, K x` are pairwise disjoint and do not contain ∅,
  - `⋃ s ∈ K x, s ⊆ x`,
  - `⋃ x ∈ J, x = ⋃ x ∈ J, ⋃ s ∈ K x, s`.

source
structure MeasureTheory.IsSetSemiring {α : Type u_1} (C : Set (Set α)) :
Prop

A semi-ring of sets `C` is a family of sets containing `∅`, stable by intersection and such that for all `s, t ∈ C`, `s \ t` is equal to a disjoint union of finitely many sets in `C`.

- empty_mem : ∅ ∈ C
- inter_mem (s : Set α) : s ∈ C → ∀ t ∈ C, s ∩ t ∈ C
- diff_eq_sUnion' (s : Set α) : s ∈ C → ∀ t ∈ C, ∃ (I : Finset (Set α)), ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

Instances For

source
theorem MeasureTheory.IsSetSemiring.isPiSystem {α : Type u_1} {C : Set (Set α)} (hC : IsSetSemiring C) :
IsPiSystem C
source
noncomputable def MeasureTheory.IsSetSemiring.disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
Finset (Set α)

In a semi-ring of sets `C`, for all sets `s, t ∈ C`, `s \ t` is equal to a disjoint union of finitely many sets in `C`. The finite set of sets in the union is not unique, but this definition gives an arbitrary `Finset (Set α)` that satisfies the equality.

We remove the empty set to ensure that `t ∉ hC.disjointOfDiff hs ht` even if `t = ∅`.

Equations

- hC.disjointOfDiff hs ht = ⋯.choose \ {∅}

Instances For

source
theorem MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
∅ ∉ hC.disjointOfDiff hs ht
source
@[deprecated MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff (since := "2025-05-24")]
theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
∅ ∉ hC.disjointOfDiff hs ht

Alias of `MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff`.

source
theorem MeasureTheory.IsSetSemiring.subset_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
↑(hC.disjointOfDiff hs ht) ⊆ C
source
theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
(↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
source
theorem MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
⋃₀ ↑(hC.disjointOfDiff hs ht) = s \ t
source
theorem MeasureTheory.IsSetSemiring.notMem_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
t ∉ hC.disjointOfDiff hs ht
source
@[deprecated MeasureTheory.IsSetSemiring.notMem_disjointOfDiff (since := "2025-05-24")]
theorem MeasureTheory.IsSetSemiring.nmem_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
t ∉ hC.disjointOfDiff hs ht

Alias of `MeasureTheory.IsSetSemiring.notMem_disjointOfDiff`.

source
theorem MeasureTheory.IsSetSemiring.sUnion_insert_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : t ⊆ s) :
⋃₀ insert t ↑(hC.disjointOfDiff hs ht) = s
source
theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
Disjoint t (⋃₀ ↑(hC.disjointOfDiff hs ht))
source
theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
(insert t ↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
source
theorem MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
∃ (J : Finset (Set α)), ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I = ⋃₀ ↑J

In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`, there is a finite set of sets in `C` whose union is `s \ ⋃₀ I`. See `IsSetSemiring.disjointOfDiffUnion` for a definition that gives such a set.

source
noncomputable def MeasureTheory.IsSetSemiring.disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
Finset (Set α)

In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`, `disjointOfDiffUnion` is a finite set of sets in `C` such that `s \ ⋃₀ I = ⋃₀ (hC.disjointOfDiffUnion hs I hI)`. `disjointOfDiff` is a special case of `disjointOfDiffUnion` where `I` is a singleton.

Equations

- hC.disjointOfDiffUnion hs hI = ⋯.choose \ {∅}

Instances For

source
theorem MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
∅ ∉ hC.disjointOfDiffUnion hs hI
source
@[deprecated MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion (since := "2025-05-24")]
theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
∅ ∉ hC.disjointOfDiffUnion hs hI

Alias of `MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion`.

source
theorem MeasureTheory.IsSetSemiring.disjointOfDiffUnion_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
↑(hC.disjointOfDiffUnion hs hI) ⊆ C
source
theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
(↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id
source
theorem MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
s \ ⋃₀ ↑I = ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
source
theorem MeasureTheory.IsSetSemiring.sUnion_disjointOfDiffUnion_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
⋃₀ ↑(hC.disjointOfDiffUnion hs hI) ⊆ s
source
theorem MeasureTheory.IsSetSemiring.subset_of_diffUnion_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (t : Set α) (ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)) :
t ⊆ s \ ⋃₀ ↑I
source
theorem MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : IsSetSemiring C) {I : Finset (Set α)} (hs : s ∈ C) (hI : ↑I ⊆ C) (t : Set α) (ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)) :
t ⊆ s
source
theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
Disjoint (⋃₀ ↑I) (⋃₀ ↑(hC.disjointOfDiffUnion hs hI))
source
theorem MeasureTheory.IsSetSemiring.disjoint_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
Disjoint I (hC.disjointOfDiffUnion hs hI)
source
theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (h_dis : (↑I).PairwiseDisjoint id) :
(↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id
source
theorem MeasureTheory.IsSetSemiring.sUnion_union_sUnion_disjointOfDiffUnion_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s) :
⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) = s
source
theorem MeasureTheory.IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s) [DecidableEq (Set α)] :
⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) = s
source
theorem MeasureTheory.IsSetSemiring.disjointOfUnion_props {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : IsSetSemiring C) (h1 : ↑J ⊆ C) :
∃ (K : Set α → Finset (Set α)), (↑J).PairwiseDisjoint K ∧ (∀ i ∈ J, ↑(K i) ⊆ C) ∧ (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧ (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
source
noncomputable def MeasureTheory.IsSetSemiring.disjointOfUnion {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (j : Set α) :
Finset (Set α)

For some `hJ : J ⊆ C` and `j : Set α`, where `hC : IsSetSemiring C`, this is a `Finset (Set α)` such that `K j := hC.disjointOfUnion hJ` are disjoint and `⋃₀ K j ⊆ j`, for `j ∈ J`. Using these we write `⋃₀ J` as a disjoint union `⋃₀ J = ⋃₀ ⋃ x ∈ J, (K x)`. See `MeasureTheory.IsSetSemiring.disjointOfUnion_props`.

Equations

- hC.disjointOfUnion hJ j = ⋯.choose j

Instances For

source
theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) :
(↑J).PairwiseDisjoint (hC.disjointOfUnion hJ)
source
theorem MeasureTheory.IsSetSemiring.disjointOfUnion_subset {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
↑(hC.disjointOfUnion hJ j) ⊆ C
source
theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) :
(⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x)).PairwiseDisjoint id
source
theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
(↑(hC.disjointOfUnion hJ j)).PairwiseDisjoint id
source
theorem MeasureTheory.IsSetSemiring.disjointOfUnion_subset_of_mem {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
⋃₀ ↑(hC.disjointOfUnion hJ j) ⊆ j
source
theorem MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfUnion {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) {x : Set α} (hx : x ∈ hC.disjointOfUnion hJ j) :
x ⊆ j
source
theorem MeasureTheory.IsSetSemiring.empty_notMem_disjointOfUnion {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
∅ ∉ hC.disjointOfUnion hJ j
source
@[deprecated MeasureTheory.IsSetSemiring.empty_notMem_disjointOfUnion (since := "2025-05-24")]
theorem MeasureTheory.IsSetSemiring.empty_nmem_disjointOfUnion {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) (hj : j ∈ J) :
∅ ∉ hC.disjointOfUnion hJ j

Alias of `MeasureTheory.IsSetSemiring.empty_notMem_disjointOfUnion`.

source
theorem MeasureTheory.IsSetSemiring.sUnion_disjointOfUnion {α : Type u_1} {C : Set (Set α)} {J : Finset (Set α)} (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) :
⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion hJ x) = ⋃₀ ↑J
source
structure MeasureTheory.IsSetRing {α : Type u_1} (C : Set (Set α)) :
Prop

A ring of sets `C` is a family of sets containing `∅`, stable by union and set difference. It is then also stable by intersection (see `IsSetRing.inter_mem`).

- empty_mem : ∅ ∈ C
- union_mem ⦃s t : Set α⦄ : s ∈ C → t ∈ C → s ∪ t ∈ C
- diff_mem ⦃s t : Set α⦄ : s ∈ C → t ∈ C → s \ t ∈ C

Instances For

source
theorem MeasureTheory.IsSetRing.inter_mem {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) :
s ∩ t ∈ C
source
theorem MeasureTheory.IsSetRing.isSetSemiring {α : Type u_1} {C : Set (Set α)} (hC : IsSetRing C) :
IsSetSemiring C
source
theorem MeasureTheory.IsSetRing.biUnion_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} (hC : IsSetRing C) {s : ι → Set α} (S : Finset ι) (hs : ∀ n ∈ S, s n ∈ C) :
⋃ i ∈ S, s i ∈ C
source
theorem MeasureTheory.IsSetRing.biInter_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} (hC : IsSetRing C) {s : ι → Set α} (S : Finset ι) (hS : S.Nonempty) (hs : ∀ n ∈ S, s n ∈ C) :
⋂ i ∈ S, s i ∈ C
source
theorem MeasureTheory.IsSetRing.finsetSup_mem {α : Type u_1} {C : Set (Set α)} (hC : IsSetRing C) {ι : Type u_2} {s : ι → Set α} {t : Finset ι} (hs : ∀ i ∈ t, s i ∈ C) :
t.sup s ∈ C
source
theorem MeasureTheory.IsSetRing.partialSups_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] (hC : IsSetRing C) {s : ι → Set α} (hs : ∀ (n : ι), s n ∈ C) (n : ι) :
(partialSups s) n ∈ C
source
theorem MeasureTheory.IsSetRing.disjointed_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] (hC : IsSetRing C) {s : ι → Set α} (hs : ∀ (j : ι), s j ∈ C) (i : ι) :
disjointed s i ∈ C
source
theorem MeasureTheory.IsSetRing.iUnion_le_mem {α : Type u_1} {C : Set (Set α)} (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ (n : ℕ), s n ∈ C) (n : ℕ) :
⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C
source
theorem MeasureTheory.IsSetRing.iInter_le_mem {α : Type u_1} {C : Set (Set α)} (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ (n : ℕ), s n ∈ C) (n : ℕ) :
⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C
source
theorem MeasureTheory.IsSetRing.accumulate_mem {α : Type u_1} {C : Set (Set α)} (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ (i : ℕ), s i ∈ C) (n : ℕ) :
Set.Accumulate s n ∈ C