mathlib

ed33a99d - chore(measure_theory/l1_space): make `measure` argument of `integrable` optional (#3508)

chore(measure_theory/l1_space): make `measure` argument of `integrable` optional (#3508) Other changes: * a few trivial lemmas; * fix notation for `∀ᵐ`: now Lean can use it for printing, not only for parsing.