Theorem WithLp.measurable_equiv_symm

Modification history

2025-07-31 10:55
Mathlib/Analysis/Normed/Lp/MeasurableSpace.lean
chore: remove old 2024-04 deprecations (#27713) …
Deleted WithLp.measurable_equiv_symmView on Github →
2025-06-23 14:42
Mathlib/Analysis/Normed/Lp/MeasurableSpace.lean
feat: a measurable space structure on `WithLp` (#26249) …
Added WithLp.measurable_equiv_symmView on Github →