nearestPtInd_le — Mathlib

English

For e : ℕ → α, N ∈ ℕ and x ∈ α, the index of the nearest point at N is always at most N.

Русский

Для e : ℕ → α, N ∈ ℕ и x ∈ α индекс ближайшей точки на уровне N не превосходит N.

LaTeX

$$$ \\mathrm{nearestPtInd}(e,N,x) \\le N$$$

Lean4

theorem nearestPtInd_le (e : ℕ → α) (N : ℕ) (x : α) : nearestPtInd e N x ≤ N := by
  induction N with
  | zero => simp
  | succ N ihN =>
    simp only [nearestPtInd_succ]
    split_ifs
    exacts [le_rfl, ihN.trans N.le_succ]

Похожие утверждения