ball_add_closedBall — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ball_add_closedBall (hε : 0 < ε) (hδ : 0 ≤ δ) (a b : E) : ball a ε + closedBall b δ = ball (a + b) (ε + δ) := by
  rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_add]

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