ball_sub_closedBall — Mathlib

English

For ε>0 and δ>0 and a,b ∈ E, ball a ε − ball b δ = ball (a−b) (ε+δ).

Русский

Для ε>0 и δ>0 и любых a,b ∈ E, ball a ε − ball b δ = ball (a−b) (ε+δ).

LaTeX

$$$$\forall a,b\in E:\; \operatorname{ball}(a,\varepsilon) - \operatorname{ball}(b,\delta) = \operatorname{ball}(a-b,\varepsilon+\delta), \quad \varepsilon>0,\ \delta>0.$$$$

Lean4

theorem ball_sub_closedBall (hε : 0 < ε) (hδ : 0 ≤ δ) (a b : E) : ball a ε - closedBall b δ = ball (a - b) (ε + δ) := by
  simp_rw [sub_eq_add_neg, neg_closedBall, ball_add_closedBall hε hδ]

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