Theorem MeasureTheory.Lp.isometry_compMeasurePreserving

Modification history

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