α : Type u_2
β : Type u_1
γ : Type ?u.840553
δ : Type ?u.840556
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Memℒp f 1
⊢ Memℒp f 1
α : Type u_2
β : Type u_1
γ : Type ?u.840553
δ : Type ?u.840556
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
⊢ Integrable f
rw [← memℒp_one_iff_integrable] at h ⊢
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.840553
δ : Type ?u.840556
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Memℒp f 1
⊢ Memℒp f 1
exact h.right_of_add_measure