English
Let e: N → α be a sequence in a metric-like space, and let x ∈ closure(range e). Then the sequence of nearest-point selections e N x converges to x; namely, (nearestPt e N x) tends to x as N → ∞ in the given topology.
Русский
Пусть e : ℕ → α заходит в метрическое пространство, и пусть x принадлежит замыканию образа e. Тогда последовательность ближайших точек к x, выбранная функцией nearestPt e N x, сходится к x при N → ∞ в данной топологии.
LaTeX
$$$\\text{If } x \\in \\overline{\\mathrm{range}(e)}, \\; \\mathrm{Tendsto}\\bigl( N \\mapsto \\mathrm{nearestPt}(e,N,x) \\bigr)\\;\\text{atTop}\\; (\\mathcal{N}(x)).$$$
Lean4
theorem tendsto_nearestPt {e : ℕ → α} {x : α} (hx : x ∈ closure (range e)) :
Tendsto (fun N => nearestPt e N x) atTop (𝓝 x) :=
by
refine (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => ?_
rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩
rw [edist_comm] at hN
exact ⟨N, trivial, fun n hn => (edist_nearestPt_le e x hn).trans_lt hN⟩
