Commit 2023-05-29 12:10 ebce4c08

View on Github →

feat: port MeasureTheory.Function.LpOrder (#4374)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/LpOrder.lean

added theorem MeasureTheory.Lp.coeFn_abs

added theorem MeasureTheory.Lp.coeFn_inf

added theorem MeasureTheory.Lp.coeFn_le

added theorem MeasureTheory.Lp.coeFn_nonneg

added theorem MeasureTheory.Lp.coeFn_sup

added theorem MeasureTheory.Memℒp.abs

added theorem MeasureTheory.Memℒp.inf

added theorem MeasureTheory.Memℒp.sup