English
In a normed vector space, for ε ≥ 0 and δ > 0, the set difference of a closed ball with center a and radius ε and an open ball with center b and radius δ is the open ball with center a − b and radius ε + δ: \n- B̄(a, ε) − B(b, δ) = B(a − b, ε + δ).
Русский
В нормированном векторном пространстве при ε ≥ 0 и δ > 0 выполняется тождество множеств: замкнутый шар B̄(a, ε) минус открытый шар B(b, δ) равен шарy с центром a − b и радиусом ε + δ: B̄(a, ε) − B(b, δ) = B(a − b, ε + δ).
LaTeX
$$$\\overline{B}(a, \\varepsilon) - B(b, \\delta) = B(a - b, \\varepsilon + \\delta)$$$
Lean4
theorem closedBall_sub_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (a b : E) : closedBall a ε - ball b δ = ball (a - b) (ε + δ) := by
simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball hε hδ]
