norm_approxOn_y₀_le — Mathlib

English

The norm of the difference F_n - y0 is bounded by the sum of the distances f x - y0 on both sides.

Русский

Норма разности F_n и y0 ограничена суммой расстояний f(x)−y0 по обе стороны.

LaTeX

$$$\\|approxOn\\ f hf s y_0 h_0 n x - y_0\\| \\le \\|f x - y_0\\| + \\|f x - y_0\\|.$$$

Lean4

theorem norm_approxOn_y₀_le [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s)
    [SeparableSpace s] (x : β) (n : ℕ) : ‖approxOn f hf s y₀ h₀ n x - y₀‖ ≤ ‖f x - y₀‖ + ‖f x - y₀‖ := by
  simpa [enorm, edist_eq_enorm_sub, ← ENNReal.coe_add, norm_sub_rev] using edist_approxOn_y0_le hf h₀ x n

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