Commit 2021-10-17 03:34 a1a05ad8
View on Github →chore(measure_theory/*): don't require the codomain to be a normed group (#9769)
Lemmas like continuous_on.ae_measurable are true for any codomain. Also add continuous.integrable_on_Ioc and continuous.integrable_on_interval_oc.