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.

THIS FILE IS NOT USED FOR THE MAIN RESULT

structure MeasureTheory.IsSetField {α : Type u_1} (C : Set (Set α)) extends MeasureTheory.IsSetRing C : 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
• sdiff_mem ⦃s t : Set α⦄ : s ∈ C → t ∈ C → s \ t ∈ C
• univ_mem : Set.univ ∈ C

theorem MeasureTheory.IsSetField.inter_mem {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : 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 : IsSetField C) (hs : s ∈ C) : sᶜ ∈ C

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

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