Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_space.generate_measurable_rec_subset

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)
Added measurable_space.generate_measurable_rec_subsetView on Github →