Commit 2021-10-29 01:24 c7f51395

chore(measure_theory): drop a few measurable_set assumptions (#9999) We had an extra measurable_set assumption in (one of the copies of) Caratheodory. Also remove measurable f assumption in is_finite_measure (map f μ) and make it an instance.