edist_nearestPt_le — Mathlib

English

If k ≤ N, the distance from x to the nearest Pt e(N) is at most the distance from x to e(k).

Русский

Если k ≤ N, расстояние до ближайшей точки e(N) не более, чем расстояние до e(k).

LaTeX

$$$ \\forall k\\le N:\\ edist\\left(\\mathrm{nearestPt}(e,N)(x),x\\right) \\le edist\\left(e(k),x\\right)$$$

Lean4

theorem edist_nearestPt_le (e : ℕ → α) (x : α) {k N : ℕ} (hk : k ≤ N) : edist (nearestPt e N x) x ≤ edist (e k) x := by
  induction N generalizing k with
  | zero => simp [nonpos_iff_eq_zero.1 hk, le_refl]
  | succ N ihN =>
    simp only [nearestPt, nearestPtInd_succ, map_apply]
    split_ifs with h
    · rcases hk.eq_or_lt with (rfl | hk)
      exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]
    · push_neg at h
      rcases h with ⟨l, hlN, hxl⟩
      rcases hk.eq_or_lt with (rfl | hk)
      exacts [(ihN hlN).trans hxl, ihN (Nat.lt_succ_iff.1 hk)]

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