Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-14 14:09 fecdd4b2

View on Github →

feat(measure_theory/card_measurable_space): generate_measurable_rec s gives precisely the generated sigma-algebra (#12462)

Estimated changes

Modified src/measure_theory/card_measurable_space.lean

added theorem measurable_space.Union_mem_generate_measurable_rec

deleted theorem measurable_space.cardinal_Union_generate_measurable_rec_le

modified theorem measurable_space.cardinal_measurable_set_le_continuum

added theorem measurable_space.compl_mem_generate_measurable_rec

added theorem measurable_space.empty_mem_generate_measurable_rec

added theorem measurable_space.generate_measurable_eq_rec

added theorem measurable_space.generate_measurable_rec_subset

deleted theorem measurable_space.generate_measurable_subset_rec

added theorem measurable_space.self_subset_generate_measurable_rec

Modified src/set_theory/cardinal_ordinal.lean