English
A simple equivalence: for all α, eq between mem of closed ball and norm inequality.
Русский
Простой эквивалент: связь между принадлежностью к замкнутому шару и неравенством по норме.
LaTeX
$$$$\forall x,y, y \in \overline{B}(x,ε) \iff \|y-x\| \le ε.$$$$
Lean4
theorem norm_sub_le_of_mem_A {c : 𝕜} (hc : 1 < ‖c‖) {r ε : ℝ} (hε : 0 < ε) (hr : 0 < r) {x : E} {L₁ L₂ : E →L[𝕜] F}
(h₁ : x ∈ A f L₁ r ε) (h₂ : x ∈ A f L₂ r ε) : ‖L₁ - L₂‖ ≤ 4 * ‖c‖ * ε :=
by
refine opNorm_le_of_shell (half_pos hr) (by positivity) hc ?_
intro y ley ylt
rw [div_div, div_le_iff₀' (by positivity)] at ley
calc
‖(L₁ - L₂) y‖ = ‖f (x + y) - f x - L₂ (x + y - x) - (f (x + y) - f x - L₁ (x + y - x))‖ := by simp
_ ≤ ‖f (x + y) - f x - L₂ (x + y - x)‖ + ‖f (x + y) - f x - L₁ (x + y - x)‖ := (norm_sub_le _ _)
_ ≤ ε * r + ε * r := by
apply add_le_add
· apply le_of_mem_A h₂
· simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
· simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
· apply le_of_mem_A h₁
· simp only [le_of_lt (half_pos hr), mem_closedBall, dist_self]
· simp only [dist_eq_norm, add_sub_cancel_left, mem_closedBall, ylt.le]
_ = 2 * ε * r := by ring
_ ≤ 2 * ε * (2 * ‖c‖ * ‖y‖) := by gcongr
_ = 4 * ‖c‖ * ε * ‖y‖ := by ring
