thickening_ball — Mathlib

English

If hε > 0 and hδ > 0, then thickening ε (ball x δ) = ball x (ε + δ).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem thickening_ball (hε : 0 < ε) (hδ : 0 < δ) (x : E) : thickening ε (ball x δ) = ball x (ε + δ) := by
  rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]

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