ball_add_ball — Mathlib

English

Let ε > 0 and δ > 0. Then thickening ε (thickening δ s) = thickening (ε+δ) s.

Русский

Пусть ε > 0 и δ > 0. Тогда thickening ε (thickening δ s) = thickening (ε+δ) s.

LaTeX

$$$$\forall s\subseteq E:\; \operatorname{thickening}(\varepsilon, \operatorname{thickening}(\delta, s)) = \operatorname{thickening}(\varepsilon+\delta, s), \quad \varepsilon>0,\ \delta>0.$$$$

Lean4

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

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