edist_approxOn_y0_le — Mathlib

English

The distance from y0 to F_n(x) is controlled by twice the distance from y0 to f(x).

Русский

Расстояние от y0 до F_n(x) контролируется удвоенным расстоянием от y0 до f(x).

LaTeX

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

Lean4

theorem edist_approxOn_y0_le {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [SeparableSpace s]
    (x : β) (n : ℕ) : edist y₀ (approxOn f hf s y₀ h₀ n x) ≤ edist y₀ (f x) + edist y₀ (f x) :=
  calc
    edist y₀ (approxOn f hf s y₀ h₀ n x) ≤ edist y₀ (f x) + edist (approxOn f hf s y₀ h₀ n x) (f x) :=
      edist_triangle_right _ _ _
    _ ≤ edist y₀ (f x) + edist y₀ (f x) := add_le_add_left (edist_approxOn_le hf h₀ x n) _

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