Theorems · Definition · measure theory

MeasureTheory.IsSetSemiring.disjointOfUnion

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

Defined in

Mathlib.MeasureTheory.SetSemiring

Cited by

10 results in Mathlib

Foundations

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