α : Type u_1
β : Type u_2
γ : Type ?u.1281080
δ : Type ?u.1281083
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ Memℒp (↑↑f) 1
α : Type u_1
β : Type u_2
γ : Type ?u.1281080
δ : Type ?u.1281083
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ Integrable ↑↑f
rw [← memℒp_one_iff_integrable]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1281080
δ : Type ?u.1281083
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : { x // x ∈ Lp β 1 }
⊢ Memℒp (↑↑f) 1
exact Lp.memℒp f