mathlib
da4d5501 - chore(measure_theory/*): better names and notations, add easy lemmas (#9554)

Commit
4 years ago
chore(measure_theory/*): better names and notations, add easy lemmas (#9554) * Localize notation for absolutely continuous in the `measure_theory` namespace, and add separate notations for the case of measures and of vector measures. * Standardize some names, using `measure` instead of `meas`. * Add two lemmas on measures with density.
Author
Parents
Loading