cthickening_ball — Mathlib

English

If hε ≥ 0 and hδ ≥ 0, then cthickening ε (ball x δ) = closedBall x (ε+δ).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem cthickening_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (x : E) : cthickening ε (ball x δ) = closedBall x (ε + δ) := by
  rw [← thickening_singleton, cthickening_thickening hε hδ, cthickening_singleton _ (add_nonneg hε hδ.le)]

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