Commit 2023-06-11 13:19 60fe1293

View on Github →

chore: copy integral notation precedence from mathport (#4963) Also drop some of the parentheses that are no longer needed.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Average.lean

modified theorem MeasureTheory.average_congr

modified theorem MeasureTheory.average_const

modified theorem MeasureTheory.average_eq'

modified theorem MeasureTheory.average_eq

modified theorem MeasureTheory.average_eq_integral

modified theorem MeasureTheory.average_neg

modified theorem MeasureTheory.average_zero

Modified Mathlib/MeasureTheory/Integral/Bochner.lean

modified theorem MeasureTheory.integrable_of_integral_eq_one

modified theorem MeasureTheory.integral_coe_le_of_lintegral_coe_le

modified theorem MeasureTheory.integral_congr_ae

modified theorem MeasureTheory.integral_const

modified theorem MeasureTheory.integral_eq

modified theorem MeasureTheory.integral_eq_zero_of_ae

modified theorem MeasureTheory.integral_neg'

modified theorem MeasureTheory.integral_neg

modified theorem MeasureTheory.integral_non_aestronglyMeasurable

modified theorem MeasureTheory.integral_nonpos

modified theorem MeasureTheory.integral_nonpos_of_ae

modified theorem MeasureTheory.integral_smul

modified theorem MeasureTheory.integral_undef

modified theorem MeasureTheory.integral_zero

Modified Mathlib/MeasureTheory/Integral/IntervalAverage.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

modified theorem MeasureTheory.ae_eq_of_ae_le_of_lintegral_le

modified theorem MeasureTheory.ae_lt_top'

modified theorem MeasureTheory.ae_lt_top

modified theorem MeasureTheory.exists_pos_set_lintegral_lt_of_measure_lt

modified theorem MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos

modified theorem MeasureTheory.isFiniteMeasure_withDensity

modified theorem MeasureTheory.lintegral_congr

modified theorem MeasureTheory.lintegral_congr_ae

modified theorem MeasureTheory.lintegral_const

modified theorem MeasureTheory.lintegral_const_lt_top

modified theorem MeasureTheory.lintegral_eq_zero_iff

modified theorem MeasureTheory.lintegral_mono

modified theorem MeasureTheory.lintegral_mono_nnreal

modified theorem MeasureTheory.lintegral_one

modified theorem MeasureTheory.lintegral_sub'

modified theorem MeasureTheory.lintegral_sub

modified theorem MeasureTheory.lintegral_unique

modified theorem MeasureTheory.lintegral_zero

modified theorem MeasureTheory.set_lintegral_const

modified theorem MeasureTheory.set_lintegral_empty

modified theorem MeasureTheory.set_lintegral_one

modified theorem MeasureTheory.set_lintegral_univ

modified theorem MeasureTheory.tendsto_set_lintegral_zero