Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 05:29 23749aa0

View on Github →

chore(measure_theory/*): use _measure instead of _meas (#3892)

Estimated changes

Modified src/measure_theory/bochner_integration.lean

deleted theorem measure_theory.integral_add_meas

added theorem measure_theory.integral_add_measure

deleted theorem measure_theory.integral_map_meas

added theorem measure_theory.integral_map_measure

deleted theorem measure_theory.integral_zero_meas

added theorem measure_theory.integral_zero_measure

deleted theorem measure_theory.simple_func.integral_add_meas

added theorem measure_theory.simple_func.integral_add_measure

Modified src/measure_theory/integration.lean

deleted theorem measure_theory.lintegral_add_meas

added theorem measure_theory.lintegral_add_measure

deleted theorem measure_theory.lintegral_smul_meas

added theorem measure_theory.lintegral_smul_measure

deleted theorem measure_theory.lintegral_sum_meas

added theorem measure_theory.lintegral_sum_measure

deleted theorem measure_theory.lintegral_zero_meas

added theorem measure_theory.lintegral_zero_measure

Modified src/measure_theory/l1_space.lean

deleted theorem measure_theory.integrable.add_meas

added theorem measure_theory.integrable.add_measure

deleted theorem measure_theory.integrable.left_of_add_meas

added theorem measure_theory.integrable.left_of_add_measure

deleted theorem measure_theory.integrable.mono_meas

added theorem measure_theory.integrable.mono_measure

deleted theorem measure_theory.integrable.right_of_add_meas

added theorem measure_theory.integrable.right_of_add_measure

deleted theorem measure_theory.integrable.smul_meas

added theorem measure_theory.integrable.smul_measure

deleted theorem measure_theory.integrable_add_meas

added theorem measure_theory.integrable_add_measure

deleted theorem measure_theory.integrable_map_meas

added theorem measure_theory.integrable_map_measure

deleted theorem measure_theory.integrable_zero_meas

added theorem measure_theory.integrable_zero_measure

Modified src/measure_theory/set_integral.lean

deleted theorem measure_theory.integrable_on.add_meas

added theorem measure_theory.integrable_on.add_measure

deleted theorem measure_theory.integrable_on.mono_meas

added theorem measure_theory.integrable_on.mono_measure

deleted theorem measure_theory.integrable_on_add_meas

added theorem measure_theory.integrable_on_add_measure

modified theorem measure_theory.integral_empty