English
For e : ℕ → α, N ∈ ℕ and x ∈ α, the nearest index among the first N+1 points is N+1 if the new point e(N+1) is strictly closer to x than every previous e(k) with k ≤ N; otherwise it remains the previous nearest index.
Русский
Для e : ℕ → α, N ∈ ℕ и x ∈ α ближайшим индекcом среди первых N+1 точек является N+1, если новая точка e(N+1) ближе к x, чем любая предыдущая e(k) при k ≤ N; иначе берется предыдущий ближайший индекc.
LaTeX
$$$ \\mathrm{nearestPtInd}(e,N+1,x) = \\begin{cases} N+1, & \\forall k \\le N,\\ edist\\left(e(N+1),x\\right) < edist\\left(e(k),x\\right) \\\\ nearestPtInd(e,N,x), & \\text{otherwise} \\end{cases}$$$
Lean4
theorem nearestPtInd_succ (e : ℕ → α) (N : ℕ) (x : α) :
nearestPtInd e (N + 1) x = if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else nearestPtInd e N x :=
by
simp only [nearestPtInd, coe_piecewise, Set.piecewise]
congr
simp
