Mathlib v3 is deprecated. Go to Mathlib v4

Theorem integral_im

Modification history

2021-07-11 20:13

src/measure_theory/set_integral.lean

feat(measure_theory/{lp_space,set_integral}): extend linear map lemmas from R to is_R_or_C (#8210)

Added integral_im View on Github →