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) _