English
Define the index of the nearest point to x among e0,...,eN; ties broken by smallest index.
Русский
Определить индекс ближайшей точки к x среди e0,...,eN; при равенствеDistances выбирается наименьший индекс.
LaTeX
$$nearestPtInd e N : α → ℕ with nearestPtInd e 0 = const α 0$$
Lean4
/-- `nearestPtInd e N x` is the index `k` such that `e k` is the nearest point to `x` among the
points `e 0`, ..., `e N`. If more than one point are at the same distance from `x`, then
`nearestPtInd e N x` returns the least of their indexes. -/
noncomputable def nearestPtInd (e : ℕ → α) : ℕ → α →ₛ ℕ
| 0 => const α 0
| N + 1 =>
piecewise (⋂ k ≤ N, {x | edist (e (N + 1)) x < edist (e k) x})
(MeasurableSet.iInter fun _ =>
MeasurableSet.iInter fun _ => measurableSet_lt measurable_edist_right measurable_edist_right)
(const α <| N + 1) (nearestPtInd e N)
