measure_space): The pushfoward measure of a finite measure is a finite measure (#9186)

Commit

4 years ago

feat(measure_theory/measure/measure_space): The pushfoward measure of a finite measure is a finite measure (#9186)

Author

kex-y

Parents