MeasureTheory.IsSetSemiring.sUnion_diffFinset
theorem MeasureTheory.IsSetSemiring.sUnion_diffFinset :
∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
(↑(hC.diffFinset hs ht)).sUnion = s \ t
This theorem states that in the context of a semi-ring of sets `C`, for any two sets `s` and `t` in `C`, the union of the finite set of sets returned by the `diffFinset` function in the `MeasureTheory.IsSetSemiring` structure is equal to the set difference `s \ t`. The `diffFinset` function yields a finite set of sets in `C` such that their disjoint union equals to `s \ t`. Specifically, for any type `α`, and for any sets `s`, `t`, and `C` of type `Set α`, if `C` forms a semi-ring of sets, and `s` and `t` are elements of `C`, then the union of the sets in the finite set returned by `diffFinset` equals the set difference of `s` and `t`.
More concisely: In a semi-ring of sets `C`, for any `s` and `t` in `C`, the union of the sets returned by `diffFinset s t` equals `s \ t`.
|
MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_diffFinset₀
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).sUnion = (↑(hC.diffFinset₀ hs hI)).sUnion
The theorem `MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_diffFinset₀` states that for any type `α`, any semiring of sets `C`, any set `s` in `C`, and any finite set of sets `I` that is a subset of `C`, if `C` is a semiring of sets, then the difference between `s` and the union of `I` (i.e., `s \ ⋃₀ ↑I`) is equal to the union of the finite set of sets calculated by `MeasureTheory.IsSetSemiring.diffFinset₀` applied with `C`, `s` and `I` (i.e., `⋃₀ ↑(MeasureTheory.IsSetSemiring.diffFinset₀ hC hs hI)`). In simpler terms, it's stating that the difference between a set and a union of sets can be found by taking the union of the differences between that set and each set in the union.
More concisely: For any semiring of sets `C`, set `s` in `C`, and finite subset `I` of `C`, `s \ (⋃ I) = ⋃ (MeasureTheory.IsSetSemiring.diffFinset₀ C s I)`.
|
MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq
theorem MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq :
∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)},
MeasureTheory.IsSetSemiring C →
s ∈ C → ↑I ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ (↑I).sUnion = (↑J).sUnion
This theorem states that in a semiring of sets `C`, for any given set `s` that is a member of `C` and any finite subset of sets `I` that is also a subset of `C`, there exists another finite set of sets `J` which is a subset of `C`, that is pairwise disjoint (meaning any two distinct sets from `J` have no common elements), and whose union is equal to the set difference of `s` and the union of `I`. In other words, this theorem claims that we can find a finite set of mutually exclusive sets in `C` that, when unionized, recreate the set `s` with the sets in `I` removed.
More concisely: For any set `s` in a semiring of sets `C` and finite subset `I` of `C`, there exists a finite, pairwise disjoint subset `J` of `C` such that `s \ (∨ x in I. X : X ∩ s = ∅) = ⋃ j in J. Xj`.
|