English
If 0 < r and ε ∈ R, and L1,L2 ∈ F with x ∈ A f L1 r ε and x ∈ A f L2 r ε, then ∥L1 - L2∥ ≤ 4ε.
Русский
Если 0 < r и ε произвольное, и L1,L2 такие, что x ∈ A(f,L1,r,ε) и x ∈ A(f,L2,r,ε), то ∥L1 - L2∥ ≤ 4ε.
LaTeX
$$$0 < r \\quad\\Rightarrow\\quad \\|L_1 - L_2\\| \\le 4 \\varepsilon \\text{ при } x \\in A f L_1 r \\varepsilon \\text{ и } x \\in A f L_2 r \\varepsilon$$$
Lean4
theorem norm_sub_le_of_mem_A {r x : ℝ} (hr : 0 < r) (ε : ℝ) {L₁ L₂ : F} (h₁ : x ∈ A f L₁ r ε) (h₂ : x ∈ A f L₂ r ε) :
‖L₁ - L₂‖ ≤ 4 * ε :=
by
suffices H : ‖(r / 2) • (L₁ - L₂)‖ ≤ r / 2 * (4 * ε) by
rwa [norm_smul, Real.norm_of_nonneg (half_pos hr).le, mul_le_mul_iff_right₀ (half_pos hr)] at H
calc
‖(r / 2) • (L₁ - L₂)‖ =
‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂ - (f (x + r / 2) - f x - (x + r / 2 - x) • L₁)‖ :=
by simp [smul_sub]
_ ≤ ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₂‖ + ‖f (x + r / 2) - f x - (x + r / 2 - x) • L₁‖ := (norm_sub_le _ _)
_ ≤ ε * r + ε * r := by
apply add_le_add
· apply le_of_mem_A h₂ <;> simp [(half_pos hr).le]
· apply le_of_mem_A h₁ <;> simp [(half_pos hr).le]
_ = r / 2 * (4 * ε) := by ring
