mathlib
59bf4540 - refactor(measure_theory): enable dot notation for measure.map (#12350)

Commit
3 years ago
refactor(measure_theory): enable dot notation for measure.map (#12350) Refactor to allow for using dot notation with `measure.map` (was previously not possible because it was bundled as a linear map). Mirrors `measure.restrict` wrapper implementation for `measure.restrictâ‚—`.
Author
Parents
Loading