Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.nearestPtInd

{α : Type u_1} →
  [inst : MeasurableSpace α] →
    [inst_1 : PseudoEMetricSpace α] → [OpensMeasurableSpace α] → (ℕ → α) → ℕ → MeasureTheory.SimpleFunc α ℕ

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 indices.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDense

Cited by

6 results in Mathlib

Foundations

Depth 155 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpace