Commit 2020-07-23 14:56 ed33a99d

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.