no goals
α : Type u_2
β : Type u_1
γ : Type ?u.827340
δ : Type ?u.827343
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
⊢ Memℒp f 1 ↔ Integrable f
simp_rw [Integrable, HasFiniteIntegral, Memℒp, snorm_one_eq_lintegral_nnnorm]