Theorem MeasureTheory.MemLp.mono_exponent

Modification history

2025-04-30 22:27

Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

chore(LpSeminorm/CompareExp): generalise to enormed spaces, part 1 (#24481)

Modified MeasureTheory.MemLp.mono_exponent View on Github →

2025-02-21 20:26

Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean

Rename `Mem𝓛p` to `MemLp` (#22164) …

Added MeasureTheory.MemLp.mono_exponent View on Github →