mathlib

a1a05ad8 - chore(measure_theory/*): don't require the codomain to be a normed group (#9769)

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`.