Semirings of sets

A semi-ring of sets C 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.

theorem MeasureTheory.IsSetSemiring.eq_add_diffFinset_of_subset {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (m : Set α → ENNReal) (m_add : ∀ (I : Finset (Set α)), ↑I ⊆ C → (↑I).PairwiseDisjoint id → ⋃₀ ↑I ∈ C → m (⋃₀ ↑I) = ∑ u ∈ I, m u) (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) [DecidableEq (Set α)] : m t = m s + ∑ i ∈ hC.diffFinset ht hs, m i

noncomputable def MeasureTheory.IsSetSemiring.indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) (n : Fin J.card) : Finset (Set α)

A finite set of sets in C such that ⋃₀ ↑(hC.indexedDiffFinset₀ J hJ n) = J.ordered n \ ⋃₀ finsetLT J n.

Equations

• hC.indexedDiffFinset₀ J hJ n = hC.diffFinset₀ ⋯ ⋯

theorem MeasureTheory.IsSetSemiring.sUnion_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) (n : Fin J.card) : ⋃₀ ↑(hC.indexedDiffFinset₀ J hJ n) = J.ordered n \ ⋃₀ ↑(J.finsetLT n)

theorem MeasureTheory.IsSetSemiring.indexedDiffFinset₀_subset {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) (n : Fin J.card) : ↑(hC.indexedDiffFinset₀ J hJ n) ⊆ C

theorem MeasureTheory.IsSetSemiring.sUnion_indexedDiffFinset₀_subset {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) (n : Fin J.card) : ⋃₀ ↑(hC.indexedDiffFinset₀ J hJ n) ⊆ J.ordered n

theorem MeasureTheory.IsSetSemiring.empty_not_mem_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) (n : Fin J.card) : ∅ ∉ hC.indexedDiffFinset₀ J hJ n

theorem MeasureTheory.IsSetSemiring.subset_ordered_of_mem_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) {n : Fin J.card} (h : s ∈ hC.indexedDiffFinset₀ J hJ n) : s ⊆ J.ordered n

theorem MeasureTheory.IsSetSemiring.iUnion_sUnion_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) : ⋃ (i : Fin J.card), ⋃₀ ↑(hC.indexedDiffFinset₀ J hJ i) = ⋃₀ ↑J

theorem MeasureTheory.IsSetSemiring.disjoint_sUnion_finsetLT_of_mem_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) {n : Fin J.card} (h : s ∈ hC.indexedDiffFinset₀ J hJ n) : Disjoint s (⋃₀ ↑(J.finsetLT n))

theorem MeasureTheory.IsSetSemiring.disjoint_ordered_of_mem_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) {n : Fin J.card} {m : Fin J.card} (h : s ∈ hC.indexedDiffFinset₀ J hJ n) (hnm : m < n) : Disjoint s (J.ordered m)

theorem MeasureTheory.IsSetSemiring.disjoint_of_mem_indexedDiffFinset₀_of_lt {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) {n : Fin J.card} {m : Fin J.card} (hnm : n < m) (hs : s ∈ hC.indexedDiffFinset₀ J hJ n) (ht : t ∈ hC.indexedDiffFinset₀ J hJ m) : Disjoint s t

theorem MeasureTheory.IsSetSemiring.disjoint_of_mem_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {t : Set α} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) {n : Fin J.card} {m : Fin J.card} (hnm : n ≠ m) (hs : s ∈ hC.indexedDiffFinset₀ J hJ n) (ht : t ∈ hC.indexedDiffFinset₀ J hJ m) : Disjoint s t

theorem MeasureTheory.IsSetSemiring.disjoint_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) {n : Fin J.card} {m : Fin J.card} (hnm : n ≠ m) : Disjoint (hC.indexedDiffFinset₀ J hJ n) (hC.indexedDiffFinset₀ J hJ m)

theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_indexedDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) : (↑Finset.univ).PairwiseDisjoint (hC.indexedDiffFinset₀ J hJ)

theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_indexedDiffFinset₀' {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) (n : Fin J.card) : (↑(hC.indexedDiffFinset₀ J hJ n)).PairwiseDisjoint id

noncomputable def MeasureTheory.IsSetSemiring.allDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) : Finset (Set α)

This is a finset of pairwise disjoint sets in the set semi-ring C, such that ⋃₀ hC.allDiffFinset₀ J hJ = ⋃₀ J.

Equations

• hC.allDiffFinset₀ J hJ = Finset.univ.disjiUnion (hC.indexedDiffFinset₀ J hJ) ⋯

theorem MeasureTheory.IsSetSemiring.pairwiseDisjoint_allDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) : (↑(hC.allDiffFinset₀ J hJ)).PairwiseDisjoint id

theorem MeasureTheory.IsSetSemiring.allDiffFinset₀_subset {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) : ↑(hC.allDiffFinset₀ J hJ) ⊆ C

theorem MeasureTheory.IsSetSemiring.sUnion_allDiffFinset₀ {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetSemiring C) (J : Finset (Set α)) (hJ : ↑J ⊆ C) : ⋃₀ ↑(hC.allDiffFinset₀ J hJ) = ⋃₀ ↑J

theorem MeasureTheory.IsSetRing.iUnion_le_mem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.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 : MeasureTheory.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 : MeasureTheory.IsSetRing C) {s : ℕ → Set α} (hs : ∀ (i : ℕ), s i ∈ C) (n : ℕ) : Set.Accumulate s n ∈ C

structure MeasureTheory.IsSetField {α : Type u_1} (C : Set (Set α)) extends MeasureTheory.IsSetRing : Prop

A field of sets is a family of sets which is stable under union, difference, and contains the empty set and the whole space.

• 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
• univ_mem : Set.univ ∈ C

theorem MeasureTheory.IsSetField.univ_mem {α : Type u_1} {C : Set (Set α)} (self : MeasureTheory.IsSetField C) : Set.univ ∈ C

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

theorem MeasureTheory.IsSetField.compl_mem {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetField C) (hs : s ∈ C) : sᶜ ∈ C

theorem MeasureTheory.IsSetField.toIsSetSemiring {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetField C) : MeasureTheory.IsSetSemiring C

theorem MeasureTheory.IsSetField.iUnion_le_mem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetField C) {s : ℕ → Set α} (hs : ∀ (n : ℕ), s n ∈ C) (n : ℕ) : ⋃ (i : ℕ), ⋃ (_ : i ≤ n), s i ∈ C

theorem MeasureTheory.IsSetField.iInter_le_mem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetField C) {s : ℕ → Set α} (hs : ∀ (n : ℕ), s n ∈ C) (n : ℕ) : ⋂ (i : ℕ), ⋂ (_ : i ≤ n), s i ∈ C

theorem MeasureTheory.IsSetField.partialSups_mem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetField C) {s : ℕ → Set α} (hs : ∀ (n : ℕ), s n ∈ C) (n : ℕ) : (partialSups s) n ∈ C

theorem MeasureTheory.IsSetField.disjointed_mem {α : Type u_1} {C : Set (Set α)} (hC : MeasureTheory.IsSetField C) {s : ℕ → Set α} (hs : ∀ (n : ℕ), s n ∈ C) (n : ℕ) : disjointed s n ∈ C