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.

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

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

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 \ {∅}

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

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

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

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

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

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

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))

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

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.

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 \ {∅}

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

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

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

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)

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

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

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

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))

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)

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

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

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

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)

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

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)

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

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

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

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

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

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

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

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.inter_mem {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : s ∩ t ∈ C

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

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

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

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

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

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

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

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

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