Commit 2024-01-26 11:59 00857680

View on Github →

feat: Add measurable_abs (#9912) See Zulip

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

Created Mathlib/MeasureTheory/Order/Group/Lattice.lean

added theorem measurable_leOnePart

added theorem measurable_mabs

added theorem measurable_oneLePart

Renamed Mathlib/MeasureTheory/Lattice.lean to Mathlib/MeasureTheory/Order/Lattice.lean