α : Type ?u.939616
β : Type u_2
ι : Type ?u.939622
E : Type u_1
F : Type ?u.939628
𝕜 : Type ?u.939631
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f 1
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) 1
n : ℕ
⊢ Memℒp (↑(approxOn f fmeas s y₀ h₀ n)) 1
α : Type ?u.939616
β : Type u_2
ι : Type ?u.939622
E : Type u_1
F : Type ?u.939628
𝕜 : Type ?u.939631
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Integrable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Integrable fun x => y₀
n : ℕ
⊢ Integrable ↑(approxOn f fmeas s y₀ h₀ n)
rw [← memℒp_one_iff_integrable] at hf hi₀⊢
no goals
α : Type ?u.939616
β : Type u_2
ι : Type ?u.939622
E : Type u_1
F : Type ?u.939628
𝕜 : Type ?u.939631
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : BorelSpace E
f : β → E
μ : Measure β
fmeas : Measurable f
hf : Memℒp f 1
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
hi₀ : Memℒp (fun x => y₀) 1
n : ℕ
⊢ Memℒp (↑(approxOn f fmeas s y₀ h₀ n)) 1
exact memℒp_approxOn fmeas hf h₀ hi₀ n