closedBall_add_ball — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem closedBall_add_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (a b : E) : closedBall a ε + ball b δ = ball (a + b) (ε + δ) := by
  rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_comm δ]

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