English
In a proper normed space, for ε, δ ≥ 0 and a, b ∈ E, the sum of closed balls equals the closed ball around the sum with radius ε + δ: B̄(a, ε) + B̄(b, δ) = B̄(a + b, ε + δ).
Русский
В корректном нормированном пространстве сумма замкнутых шаров равна замкнутому шару с центром в сумме и радиусом равным сумме радиусов: B̄(a, ε) + B̄(b, δ) = B̄(a + b, ε + δ).
LaTeX
$$$\\overline{B}(a, \\varepsilon) + \\overline{B}(b, \\delta) = \\overline{B}(a + b, \\varepsilon + \\delta)$$$
Lean4
theorem closedBall_add_closedBall [ProperSpace E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a b : E) :
closedBall a ε + closedBall b δ = closedBall (a + b) (ε + δ) := by
rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a, Metric.vadd_closedBall,
vadd_eq_add, add_comm, add_comm δ]
