closedBall_sub_closedBall — Mathlib

English

For ε ≥ 0 and δ ≥ 0 and a, b ∈ E, the set difference of closed balls equals a closed ball: B̄(a, ε) − B̄(b, δ) = B̄(a − b, ε + δ).

Русский

Для ε ≥ 0 и δ ≥ 0 и точек a, b ∈ E выполняется равенство разности замкнутых шаров: 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_sub_closedBall [ProperSpace E] (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (a b : E) :
    closedBall a ε - closedBall b δ = closedBall (a - b) (ε + δ) := by
  rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]

Похожие утверждения