edist_approxOn_mono — Mathlib

English

For m ≤ n, the distance to f x from approxOn decreases with n; i.e., edist(F_n x, f x) ≤ edist(F_m x, f x).

Русский

При m ≤ n расстояние edist(F_n x, f x) не возрастает; оно не больше edist(F_m x, f x).

LaTeX

$$$edist(approxOn f hf s y_0 h_0 n x, f x) \\le edist(approxOn f hf s y_0 h_0 m x, f x) \\quad( m \\le n ).$$$

Lean4

theorem edist_approxOn_mono {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [SeparableSpace s]
    (x : β) {m n : ℕ} (h : m ≤ n) : edist (approxOn f hf s y₀ h₀ n x) (f x) ≤ edist (approxOn f hf s y₀ h₀ m x) (f x) :=
  by
  dsimp only [approxOn, coe_comp, Function.comp_def]
  exact edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans h)

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