mathlib3

8d5830e6 - chore(measure_theory/measurable_space): use implicit measurable_space argument (#11230)

chore(measure_theory/measurable_space): use implicit measurable_space argument (#11230) The `measurable_space` argument is inferred from other arguments (like `measurable f` or a measure for example) instead of being a type class. This ensures that the lemmas are usable without `@` when several measurable space structures are used for the same type. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>