Commit 2021-10-01 01:13 5b025712

View on Github →

chore(measure_theory/decomposition/lebesgue): make measurable_space implicit (#9463) Whenever the measurable_space can be inferred from a measure argument, it should be implicit. This PR applies that rule to the Lebesgue decomposition file.

Estimated changes

Modified src/measure_theory/decomposition/lebesgue.lean

modified theorem measure_theory.measure.eq_rn_deriv

modified theorem measure_theory.measure.eq_singular_part

modified theorem measure_theory.measure.have_lebesgue_decomposition_add

modified theorem measure_theory.measure.have_lebesgue_decomposition_of_finite_measure

modified theorem measure_theory.measure.have_lebesgue_decomposition_spec

modified theorem measure_theory.signed_measure.eq_rn_deriv

modified theorem measure_theory.signed_measure.eq_singular_part

modified theorem measure_theory.signed_measure.have_lebesgue_decomposition_mk

modified theorem measure_theory.signed_measure.mutually_singular_singular_part

modified theorem measure_theory.signed_measure.not_have_lebesgue_decomposition_iff

modified theorem measure_theory.signed_measure.rn_deriv_add

modified theorem measure_theory.signed_measure.rn_deriv_neg

modified theorem measure_theory.signed_measure.rn_deriv_smul

modified theorem measure_theory.signed_measure.rn_deriv_sub

added def measure_theory.signed_measure.singular_part(s

deleted def measure_theory.signed_measure.singular_part

modified theorem measure_theory.signed_measure.singular_part_mutually_singular

modified theorem measure_theory.signed_measure.singular_part_smul

modified theorem measure_theory.signed_measure.singular_part_total_variation