ball_sub_ball — 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_ball (hε : 0 < ε) (hδ : 0 < δ) (a b : E) : ball a ε - ball b δ = ball (a - b) (ε + δ) := by
  simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball hε hδ]

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