Commit 2023-03-17 16:26 6d2275b4

View on Github →

feat: port MeasureTheory.CardMeasurableSpace (#2516)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/CardMeasurableSpace.lean

added theorem MeasurableSpace.cardinalMeasurableSet_le

added theorem MeasurableSpace.cardinal_generateMeasurableRec_le

added theorem MeasurableSpace.cardinal_generateMeasurable_le

added theorem MeasurableSpace.cardinal_generateMeasurable_le_continuum

added theorem MeasurableSpace.cardinal_measurableSet_le_continuum

added theorem MeasurableSpace.compl_mem_generateMeasurableRec

added theorem MeasurableSpace.empty_mem_generateMeasurableRec

added def MeasurableSpace.generateMeasurableRec

added theorem MeasurableSpace.generateMeasurableRec_subset

added theorem MeasurableSpace.generateMeasurable_eq_rec

added theorem MeasurableSpace.self_subset_generateMeasurableRec

added theorem MeasurableSpace.unionᵢ_mem_generateMeasurableRec