Theorem MeasureTheory.Memℒp.mono_exponent_of_measure_support_ne_top

Modification history

2025-01-13 10:56
Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
chore(LpSpace): move results about the L^p norm earlier (#20541) …
Added MeasureTheory.Memℒp.mono_exponent_of_measure_support_ne_topView on Github →