Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-16 21:43 7b9acd9e

View on Github →

chore(measure_theory/*): reflow long lines (#4642) Also do some minor golfing.

Estimated changes

Modified src/measure_theory/ae_eq_fun.lean

Modified src/measure_theory/bochner_integration.lean

modified theorem measure_theory.integral_add_measure'

modified theorem measure_theory.l1.simple_func.coe_add

modified theorem measure_theory.l1.simple_func.coe_neg

modified theorem measure_theory.l1.simple_func.coe_neg_part

modified theorem measure_theory.l1.simple_func.coe_pos_part

modified theorem measure_theory.l1.simple_func.coe_sub

modified theorem measure_theory.l1.simple_func.coe_zero

Modified src/measure_theory/content.lean

Modified src/measure_theory/giry_monad.lean

Modified src/measure_theory/integration.lean

modified theorem measure_theory.simple_func.supr_approx_apply

Modified src/measure_theory/interval_integral.lean

Modified src/measure_theory/l1_space.lean

Modified src/measure_theory/lebesgue_measure.lean

Modified src/measure_theory/measurable_space.lean

Modified src/measure_theory/measure_space.lean

Modified src/measure_theory/set_integral.lean