Theorem MeasurableEquiv.toLp_symm_apply

Modification history

2025-06-23 14:42
Mathlib/Analysis/Normed/Lp/MeasurableSpace.lean
feat: a measurable space structure on `WithLp` (#26249) …
Added MeasurableEquiv.toLp_symm_applyView on Github →