Theorem MeasureTheory.Lp.compMeasurePreserving_continuous

Modification history

2024-07-18 04:27
Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean
feat(LpSpace/ContinuousCompMeasurePreserving): new file (#14500) …
Added MeasureTheory.Lp.compMeasurePreserving_continuousView on Github →