Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-11 13:22 0fe28491

View on Github →

chore(analysis/measure_theory): finish characterization of lintegral

Estimated changes

Modified analysis/measure_theory/integration.lean

added theorem measure_theory.lintegral_const_mul

added theorem measure_theory.lintegral_supr_const

modified theorem measure_theory.simple_func.bind_const

modified def measure_theory.simple_func.const

modified theorem measure_theory.simple_func.const_apply

modified theorem measure_theory.simple_func.const_mul_eq_map

modified def measure_theory.simple_func.map