Commit 2024-11-19 00:05 42f07b97

View on Github →

refactor(MeasureTheory/MeasurableSpace/Card): avoid Ordinal.toType (#18199) We redefine generateMeasurableRec so that it's indexed by an ordinal, rather than being indexed by ω₁.toType. We also employ ω₁ and its new API throughout the file.

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace/Card.lean

deleted theorem MeasurableSpace.cardinalMeasurableSet_le

modified theorem MeasurableSpace.cardinal_generateMeasurableRec_le

added theorem MeasurableSpace.cardinal_measurableSet_le

modified theorem MeasurableSpace.compl_mem_generateMeasurableRec

modified theorem MeasurableSpace.empty_mem_generateMeasurableRec

modified def MeasurableSpace.generateMeasurableRec

added theorem MeasurableSpace.generateMeasurableRec_induction

added theorem MeasurableSpace.generateMeasurableRec_mono

added theorem MeasurableSpace.generateMeasurableRec_of_omega1_le

added theorem MeasurableSpace.generateMeasurableRec_omega1

modified theorem MeasurableSpace.generateMeasurableRec_subset

modified theorem MeasurableSpace.iUnion_mem_generateMeasurableRec

modified theorem MeasurableSpace.self_subset_generateMeasurableRec

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

added theorem Cardinal.IsRegular.cof_omega_eq