edist_approxOn_le — Mathlib

English

For any x and n, the distance edist(F_n x, f x) is bounded by the initial distance edist y0 (f x).

Русский

Для любых x и n расстояние edist(F_n x, f x) ограничено edist y0 (f x).

LaTeX

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

Lean4

theorem edist_approxOn_le {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α} (h₀ : y₀ ∈ s) [SeparableSpace s] (x : β)
    (n : ℕ) : edist (approxOn f hf s y₀ h₀ n x) (f x) ≤ edist y₀ (f x) :=
  edist_approxOn_mono hf h₀ x (zero_le n)

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