2022-12-04 09:54
src/topology/algebra/order/liminf_limsup.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_Ioi_of_lt_of_tendsto