closedBall_subset_cthickening — Mathlib

English

The closed ball of radius δ around a point x in E is contained in the δ-thickening of E.

Русский

Замкнутый шар радиуса δ вокруг точки x из E вложен в δ-уплотнение E.

LaTeX

$${\it maybe notated} \overline{B}(x,δ) \subseteq \operatorname{cthickening}_{δ} E$$

Lean4

/-- The closed ball of radius `δ` centered at a point of `E` is included in the closed
thickening of `E`. -/
theorem closedBall_subset_cthickening {α : Type*} [PseudoMetricSpace α] {x : α} {E : Set α} (hx : x ∈ E) (δ : ℝ) :
    closedBall x δ ⊆ cthickening δ E :=
  by
  refine (closedBall_subset_cthickening_singleton _ _).trans (cthickening_subset_of_subset _ ?_)
  simpa using hx

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