Theorems · Definition · measure theory

MeasureTheory.SimpleFunc.nearestPt

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

nearestPt e N x 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 nearestPt e N x returns the point with the least possible index.

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDense

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpace