Mathlib v3 is deprecated. Go to Mathlib v4

Theorem Union_Ici_eq_Ici_infi

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_Ici_eq_Ici_infiView on Github →