α : Type u_1
β : Type ?u.3383671
ι : Type ?u.3383674
E : Type u_2
F : Type ?u.3383680
𝕜 : Type ?u.3383683
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ Lp.simpleFunc E 1 μ }
⊢ Memℒp (↑(Lp.simpleFunc.toSimpleFunc f)) 1
α : Type u_1
β : Type ?u.3383671
ι : Type ?u.3383674
E : Type u_2
F : Type ?u.3383680
𝕜 : Type ?u.3383683
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ Lp.simpleFunc E 1 μ }
⊢ Integrable ↑(Lp.simpleFunc.toSimpleFunc f)
rw [← memℒp_one_iff_integrable]
no goals
α : Type u_1
β : Type ?u.3383671
ι : Type ?u.3383674
E : Type u_2
F : Type ?u.3383680
𝕜 : Type ?u.3383683
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f✝ : α → E
p : ℝ≥0∞
μ : Measure α
f : { x // x ∈ Lp.simpleFunc E 1 μ }
⊢ Memℒp (↑(Lp.simpleFunc.toSimpleFunc f)) 1
exact Lp.simpleFunc.memℒp f