English
If f x belongs to closure of s, the approximants converge to f x in the sense of Tendsto.
Русский
Если f(x) принадлежит замыканию s, то F_n(x) сходится к f(x) по Tendency как n→∞.
LaTeX
$$$\\text{If } x\\text{ satisfies } f(x)\\in\\overline{s},\\; \\mathrm{Tendsto}\\bigl( n \\mapsto approxOn f hf s y_0 h_0 n x \\bigr)_{n\\to\\infty} = f(x).$$$
Lean4
theorem tendsto_approxOn {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [SeparableSpace s] {x : β}
(hx : f x ∈ closure s) : Tendsto (fun n => approxOn f hf s y₀ h₀ n x) atTop (𝓝 <| f x) :=
by
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
rw [← @Subtype.range_coe _ s, ← image_univ, ← (denseRange_denseSeq s).closure_eq] at hx
simp -iota only [approxOn, coe_comp]
refine tendsto_nearestPt (closure_minimal ?_ isClosed_closure hx)
simp -iota only [Nat.range_casesOn, closure_union, range_comp]
exact Subset.trans (image_closure_subset_closure_image continuous_subtype_val) subset_union_right
