Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Union_Iic_eq_Iio_supr

Modification history

2022-12-04 09:54
src/data/set/intervals/disjoint.lean
feat(measure_theory/measure/measure_space): In sigma finite measure spaces, disjoint unions can have at most countably many positive measure parts. (#15492) …
Added Union_Iic_eq_Iio_suprView on Github →