Theorem MeasureTheory.MemLp.meas_ge_lt_top'_enorm

Modification history

2025-05-12 13:27
Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean
chore(LpSeminorm/ChebyshevMarkov): generalise to enorms (#24482)
Added MeasureTheory.MemLp.meas_ge_lt_top'_enormView on Github →