Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_space.cardinal_Union_generate_measurable_rec_le

Modification history

2022-04-14 14:09
src/measure_theory/card_measurable_space.lean
feat(measure_theory/card_measurable_space): `generate_measurable_rec s` gives precisely the generated sigma-algebra (#12462)
Deleted measurable_space.cardinal_Union_generate_measurable_rec_leView on Github →
2022-03-05 10:56
src/measure_theory/card_measurable_space.lean
feat(measure_theory/card_measurable_space): cardinality of generated sigma-algebras (#12422) …
Added measurable_space.cardinal_Union_generate_measurable_rec_leView on Github →