Theorems · Theorem · measure theory

MeasureTheory.SimpleFunc.nearestPtInd_succ

∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α] [inst_2 : OpensMeasurableSpace α]
  (e : ℕ → α) (N : ℕ) (x : α),
  (MeasureTheory.SimpleFunc.nearestPtInd e (N + 1)) x =
    if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (MeasureTheory.SimpleFunc.nearestPtInd e N) x

Defined in

Mathlib.MeasureTheory.Function.SimpleFuncDense

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpaceOpensMeasurableSpace