English
Norm-based bound: the NN-norm distance between approxOn and f is bounded by the distance to y0.
Русский
Граневая неравенство по норме: отношение НН-нормы между approxOn и f ограничено расстоянием до y0.
LaTeX
$$$\\|approxOn\\ f\\ hf\\ s\\ y_0\\ h_0\\ n\\ x - f\\ x\\|_{nn} \\le \\|f\\ x - y_0\\|_{nn}.$$$
Lean4
theorem nnnorm_approxOn_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 - f x‖₊ ≤ ‖f x - y₀‖₊ :=
by
have := edist_approxOn_le hf h₀ x n
rw [edist_comm y₀] at this
simp only [edist_nndist, nndist_eq_nnnorm] at this
exact mod_cast this