Theorem MeasureTheory.MemLp.meas_ge_lt_top'

Modification history

2025-05-12 13:27

Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean

chore(LpSeminorm/ChebyshevMarkov): generalise to enorms (#24482)

Modified MeasureTheory.MemLp.meas_ge_lt_top'View on Github →

2025-02-21 20:26

Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean

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

Added MeasureTheory.MemLp.meas_ge_lt_top'View on Github →