Theorems · Theorem · measure theory

MeasurableSpace.generateMeasurableRec.eq_def

∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}),
  MeasurableSpace.generateMeasurableRec s i =
    have S := ⋃ j, ⋃ (_ : j < i), MeasurableSpace.generateMeasurableRec s j;
    s ∪ {∅} ∪ compl '' S ∪ Set.range fun f => ⋃ n, ↑(f n)

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Card

Cited by

5 results in Mathlib

Foundations

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