A nearest element of a finite, nonempty format. Ties are unspecified.
def nearest {α : Type*} [Fintype α] [Nonempty α] (value : α → ℝ) (x : ℝ) : α :=
(Finset.univ.exists_min_image (fun a => |x - value a|) Finset.univ_nonempty).choosetheorem nearest_le {α : Type*} [Fintype α] [Nonempty α]
(value : α → ℝ) (x : ℝ) (a : α) :
|x - value (nearest value x)| ≤ |x - value a| :=
(Finset.univ.exists_min_image (fun a => |x - value a|)
Finset.univ_nonempty).choose_spec.2 a (Finset.mem_univ _)