Theorems · Theorem · measure theory

MeasurableSpace.DynkinSystem.has_iUnion

∀ {α : Type u_3} (d : MeasurableSpace.DynkinSystem α) {β : Type u_4} [Countable β] {f : β → Set α},
  Pairwise (Function.onFun Disjoint f) → (∀ (i : β), d.Has (f i)) → d.Has (⋃ i, f i)

Defined in

Mathlib.MeasureTheory.PiSystem

Cited by

2 results in Mathlib

Foundations

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

Assumes

Countable