no goals
α : Type ?u.930924
β : Type u_2
ι : Type ?u.930930
E : Type u_1
F : Type ?u.930936
𝕜 : Type ?u.930939
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : HasFiniteIntegral fun x => f x - y₀
⊢ Tendsto (fun n => ∫⁻ (x : β), ↑‖↑(approxOn f hf s y₀ h₀ n) x - f x‖₊ ∂μ) atTop (𝓝 0)
simpa [snorm_one_eq_lintegral_nnnorm] using
  tendsto_approxOn_Lp_snorm hf h₀ one_ne_top hμ
    (by simpa [snorm_one_eq_lintegral_nnnorm] using hi)
no goals
α : Type ?u.930924
β : Type u_2
ι : Type ?u.930930
E : Type u_1
F : Type ?u.930936
𝕜 : Type ?u.930939
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
μ : Measure β
hμ : ∀ᵐ (x : β) ∂μ, f x ∈ closure s
hi : HasFiniteIntegral fun x => f x - y₀
⊢ snorm (fun x => f x - y₀) 1 μ < ⊤
simpa [snorm_one_eq_lintegral_nnnorm] using hi