@[simp]

theorem MeasureTheory.memLp_top_one {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] [One E] : MemLp 1 ⊤ μ