Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-21 22:13 9998bee7

View on Github →

chore(measure_theory/*): remove some measurable f arguments (#3902)

Estimated changes

Modified src/measure_theory/bochner_integration.lean

modified theorem measure_theory.integral_add_measure

Modified src/measure_theory/interval_integral.lean

modified theorem interval_integral.integral_Iic_sub_Iic

modified theorem interval_integral.integral_add_adjacent_intervals

modified theorem interval_integral.integral_add_adjacent_intervals_cancel

modified theorem interval_integral.integral_interval_add_interval_comm

modified theorem interval_integral.integral_interval_sub_interval_comm'

modified theorem interval_integral.integral_interval_sub_interval_comm

modified theorem interval_integral.integral_interval_sub_left

Modified src/measure_theory/set_integral.lean

modified theorem measure_theory.integral_add_compl