cthickening_closedBall — Mathlib

English

Let hε ≥ 0 and hδ ≥ 0. Then cthickening ε (closedBall x δ) = closedBall x (ε+δ).

Русский

Пусть ε ≥ 0 и δ ≥ 0. Тогда cthickening ε (closedBall x δ) = closedBall x (ε+δ).

LaTeX

$$$$\forall x:\; \operatorname{cthickening}(\varepsilon, \operatorname{closedBall}(x,\delta)) = \operatorname{closedBall}(x,\varepsilon+\delta), \quad \varepsilon\ge 0,\ \delta\ge 0.$$$$

Lean4

@[simp]
theorem cthickening_closedBall (hε : 0 ≤ ε) (hδ : 0 ≤ δ) (x : E) :
    cthickening ε (closedBall x δ) = closedBall x (ε + δ) := by
  rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ, cthickening_singleton _ (add_nonneg hε hδ)]

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