Theorems · Definition · measure theory

MeasureTheory.IsSetSemiring.disjointOfDiffUnion

{α : Type u_1} →
  {C : Set (Set α)} →
    {s : Set α} → {I : Finset (Set α)} → MeasureTheory.IsSetSemiring C → s ∈ C → ↑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.

Defined in

Mathlib.MeasureTheory.SetSemiring

Cited by

16 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound