α : Type u_2
β✝ : Type ?u.955189
γ : Type ?u.955192
δ : Type ?u.955195
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_1
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : Memℒp f 1
⊢ Memℒp (fun a => Abs.abs (f a)) 1
α : Type u_2
β✝ : Type ?u.955189
γ : Type ?u.955192
δ : Type ?u.955195
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_1
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : Integrable f
⊢ Integrable fun a => Abs.abs (f a)
rw [← memℒp_one_iff_integrable] at hf⊢
no goals
α : Type u_2
β✝ : Type ?u.955189
γ : Type ?u.955192
δ : Type ?u.955195
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β✝
inst✝¹ : NormedAddCommGroup γ
β : Type u_1
inst✝ : NormedLatticeAddCommGroup β
f : α → β
hf : Memℒp f 1
⊢ Memℒp (fun a => Abs.abs (f a)) 1
exact hf.abs