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.diffFinset 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.diffFinset hs ht.

• MeasureTheory.IsSetSemiring.diffFinset₀ 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.diffFinset₀ hs hI.

• 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.diffFinset₀ (see above).

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 ∈ C, ∀ t ∈ C, s ∩ t ∈ C
• diff_eq_sUnion' : ∀ s ∈ C, ∀ t ∈ C, ∃ (I : Finset (Set α)), ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

theorem MeasureTheory.IsSetSemiring.empty_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetSemiring C) : ∅ ∈ C

theorem MeasureTheory.IsSetSemiring.inter_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetSemiring C) (s : Set α) : s ∈ C → ∀ t ∈ C, s ∩ t ∈ C

theorem MeasureTheory.IsSetSemiring.diff_eq_sUnion' {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetSemiring C) (s : Set α) : s ∈ C → ∀ t ∈ C, ∃ (I : Finset (Set α)), ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

theorem MeasureTheory.IsSetSemiring.isPiSystem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) : IsPiSystem C

noncomputable def MeasureTheory.IsSetSemiring.diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.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.diffFinset hs ht even if t = ∅.

Equations

• hC.diffFinset hs ht = ⋯.choose \ {∅}

theorem MeasureTheory.IsSetSemiring.empty_not_mem_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : ∅ ∉ hC.diffFinset hs ht

theorem MeasureTheory.IsSetSemiring.diffFinset_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : ↑(hC.diffFinset hs ht) ⊆ C

theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : (↑(hC.diffFinset hs ht)).PairwiseDisjoint id

theorem MeasureTheory.IsSetSemiring.sUnion_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : ⋃₀ ↑(hC.diffFinset hs ht) = s \ t

theorem MeasureTheory.IsSetSemiring.not_mem_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : t ∉ hC.diffFinset hs ht

theorem MeasureTheory.IsSetSemiring.sUnion_insert_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) (hst : t ⊆ s) : ⋃₀ insert t ↑(hC.diffFinset hs ht) = s

theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : Disjoint t (⋃₀ ↑(hC.diffFinset hs ht))

theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_insert_diffFinset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) : (insert t ↑(hC.diffFinset hs ht)).PairwiseDisjoint id

theorem MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.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.diffFinset₀ for a definition that gives such a set.

noncomputable def MeasureTheory.IsSetSemiring.diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.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, diffFinset₀ is a finite set of sets in C such that s \ ⋃₀ I = ⋃₀ (hC.diffFinset₀ hs I hI). diffFinset is a special case of diffFinset₀ where I is a singleton.

Equations

• hC.diffFinset₀ hs hI = ⋯.choose \ {∅}

theorem MeasureTheory.IsSetSemiring.empty_not_mem_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : ∅ ∉ hC.diffFinset₀ hs hI

theorem MeasureTheory.IsSetSemiring.diffFinset₀_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : ↑(hC.diffFinset₀ hs hI) ⊆ C

theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : (↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id

theorem MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : s \ ⋃₀ ↑I = ⋃₀ ↑(hC.diffFinset₀ hs hI)

theorem MeasureTheory.IsSetSemiring.sUnion_diffFinset₀_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : ⋃₀ ↑(hC.diffFinset₀ hs hI) ⊆ s

theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : Disjoint (⋃₀ ↑I) (⋃₀ ↑(hC.diffFinset₀ hs hI))

theorem MeasureTheory.IsSetSemiring.disjoint_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) : Disjoint I (hC.diffFinset₀ hs hI)

theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_union_diffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (h_dis : (↑I).PairwiseDisjoint id) : (↑I ∪ ↑(hC.diffFinset₀ hs hI)).PairwiseDisjoint id

theorem MeasureTheory.IsSetSemiring.sUnion_union_sUnion_diffFinset₀_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s) : ⋃₀ ↑I ∪ ⋃₀ ↑(hC.diffFinset₀ hs hI) = s

theorem MeasureTheory.IsSetSemiring.sUnion_union_diffFinset₀_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s) [DecidableEq (Set α)] : ⋃₀ ↑(I ∪ hC.diffFinset₀ hs hI) = s

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

theorem MeasureTheory.IsSetRing.empty_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetRing C) : ∅ ∈ C

theorem MeasureTheory.IsSetRing.union_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetRing C) ⦃s : Set α⦄ ⦃t : Set α⦄ : s ∈ C → t ∈ C → s ∪ t ∈ C

theorem MeasureTheory.IsSetRing.diff_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetRing C) ⦃s : Set α⦄ ⦃t : Set α⦄ : s ∈ C → t ∈ C → s \ t ∈ C

theorem MeasureTheory.IsSetRing.inter_mem {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : s ∩ t ∈ C

theorem MeasureTheory.IsSetRing.isSetSemiring {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetRing C) : MeasureTheory.IsSetSemiring C

theorem MeasureTheory.IsSetRing.biUnion_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} (hC : MeasureTheory.IsSetRing C) {s : ι → Set α} (S : Finset ι) (hs : ∀ n ∈ S, s n ∈ C) : ⋃ i ∈ S, s i ∈ C

theorem MeasureTheory.IsSetRing.biInter_mem {α : Type u_1} {C : Set (Set α)} {ι : Type u_2} (hC : MeasureTheory.IsSetRing C) {s : ι → Set α} (S : Finset ι) (hS : S.Nonempty) (hs : ∀ n ∈ S, s n ∈ C) : ⋂ i ∈ S, s i ∈ C