Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_space.generate_measurable_subset_rec

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.generate_measurable_subset_recView 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.generate_measurable_subset_recView on Github →