thickening_ball — Mathlib

English

In a metric space, the ε-thickening of the closed ball around x of radius δ is contained in the closed ball around x of radius δ+ε.

Русский

В метрическом пространстве ε-уплотнение замкнутого шара B[x,δ] содержится в B[x,δ+ε].

LaTeX

$$$\operatorname{thickening}_{\varepsilon}(\operatorname{ball}(x,\delta)) \subseteq \operatorname{ball}(x,\delta+\varepsilon)$$$

Lean4

theorem thickening_ball [PseudoMetricSpace α] (x : α) (ε δ : ℝ) : thickening ε (ball x δ) ⊆ ball x (ε + δ) :=
  by
  rw [← thickening_singleton, ← thickening_singleton]
  apply thickening_thickening_subset

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