Commit 2023-09-19 03:31 28b8e22a

View on Github →

chore(LpSpace): golf (#7214) Cherry-picked from #6839

Estimated changes

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

modified theorem MeasureTheory.Lp.mem_Lp_iff_snorm_lt_top

added theorem MeasureTheory.Lp.nnnorm_coe_ennreal