Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measurable_space.Union_mem_generate_measurable_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)
Added measurable_space.Union_mem_generate_measurable_recView on Github →