norm_approxOn_zero_le — Mathlib

English

With starting point y0=0, the bound simplifies to an expression with the same two-norm term.

Русский

При y0=0 получаем упрощённое неравенство на норму, зависящее от той же пары норм.

LaTeX

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

Lean4

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

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