α : Type u_2
β : Type u_1
γ : Type ?u.846855
δ : Type ?u.846858
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Memℒp f 1
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ Memℒp f 1
α : Type u_2
β : Type u_1
γ : Type ?u.846855
δ : Type ?u.846858
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Integrable f
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ Integrable f
rw [← memℒp_one_iff_integrable] at h ⊢
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.846855
δ : Type ?u.846858
m : MeasurableSpace α
μ ν : Measure α
inst✝² : MeasurableSpace δ
inst✝¹ : NormedAddCommGroup β
inst✝ : NormedAddCommGroup γ
f : α → β
h : Memℒp f 1
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ Memℒp f 1
exact h.smul_measure hc