Commit 2024-03-30 08:23 956f433e

View on Github →

feat: add by volume_tac to get a default measure in AEStronglyMeasurable (#11771) This is already the case for Integrable and AEMeasurable.

Estimated changes

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

added theorem Continuous.comp_aestronglyMeasurable₂

modified def MeasureTheory.AEFinStronglyMeasurable

modified def MeasureTheory.AEStronglyMeasurable

modified def MeasureTheory.FinStronglyMeasurable