Theorem Continuous.comp_aestronglyMeasurable₂

Modification history

2025-01-31 17:41

Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) …

Modified Continuous.comp_aestronglyMeasurable₂ View on Github →

2024-03-30 08:23

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

feat: add `by volume_tac` to get a default measure in `AEStronglyMeasurable` (#11771) …

Added Continuous.comp_aestronglyMeasurable₂ View on Github →