Theorems · Theorem · measure theory

MeasurableSpace.cardinal_generateMeasurableRec_le

∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{v}),
  Cardinal.mk ↑(MeasurableSpace.generateMeasurableRec s i) ≤ max (Cardinal.mk ↑s) 2 ^ Cardinal.aleph0

At each step of the inductive construction, the cardinality bound ≤ #s ^ ℵ₀ holds.

Defined in

Mathlib.MeasureTheory.MeasurableSpace.Card

Cited by

1 results in Mathlib

Foundations

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