Commit 2025-06-23 14:42 f355283a

View on Github →

feat: a measurable space structure on WithLp (#26249) Put a measurable space structure on a general WithLp. Define a MeasurableEquiv version of WithLp.equiv. The direction is reversed in prevision of the WithLp refactor in #24261. Define a BorelSpace instance.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Normed/Lp/MeasurableSpace.lean

added theorem MeasurableEquiv.coe_toLp

added theorem MeasurableEquiv.coe_toLp_symm

added theorem MeasurableEquiv.toLp_apply

added theorem MeasurableEquiv.toLp_symm_apply

added theorem WithLp.measurable_equiv

added theorem WithLp.measurable_equiv_symm