α : Type u_1
β : Type ?u.1130946
γ : Type ?u.1130949
δ : Type ?u.1130952
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f✝ : α → 𝕜
f : α → ℝ
hf : Memℒp f 1
⊢ Memℒp (fun x => ↑(f x)) 1
α : Type u_1
β : Type ?u.1130946
γ : Type ?u.1130949
δ : Type ?u.1130952
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f✝ : α → 𝕜
f : α → ℝ
hf : Integrable f
⊢ Integrable fun x => ↑(f x)
rw [← memℒp_one_iff_integrable] at hf ⊢
no goals
α : Type u_1
β : Type ?u.1130946
γ : Type ?u.1130949
δ : Type ?u.1130952
m : MeasurableSpace α
μ ν : Measure α
inst✝³ : MeasurableSpace δ
inst✝² : NormedAddCommGroup β
inst✝¹ : NormedAddCommGroup γ
𝕜 : Type u_2
inst✝ : IsROrC 𝕜
f✝ : α → 𝕜
f : α → ℝ
hf : Memℒp f 1
⊢ Memℒp (fun x => ↑(f x)) 1
exact hf.ofReal