Theorem MeasureTheory.AEStronglyMeasurable.piecewise_iff

Modification history

2026-09-25 23:29

Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

chore(MeasureTheory): generalize hypotheses to `NullMeasurableSet` (#42924) …

Modified MeasureTheory.AEStronglyMeasurable.piecewise_iff View on Github →

2026-09-11 14:45

Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean

refactor(MeasureTheory): define `eLpNorm f` to be infinite when not `AEStronglyMeasurable` (#42406) …

Added MeasureTheory.AEStronglyMeasurable.piecewise_iff View on Github →