ball_subset_thickening — Mathlib

English

For sets E in a metric space, thickening δ E is the union of all balls of radius δ centered at points of E.

Русский

Для множества E в метрическом пространстве thickening δ E равен объединению всех шаров радиуса δ, центрированных в точках E.

LaTeX

$$$\\mathrm{thickening}\\,δ\\,E = \\bigcup_{x\\in E} \\mathrm{ball}\\,x\\,δ$$$

Lean4

theorem ball_subset_thickening {x : X} {E : Set X} (hx : x ∈ E) (δ : ℝ) : ball x δ ⊆ thickening δ E :=
  Subset.trans (by simp) (thickening_subset_of_subset δ <| singleton_subset_iff.mpr hx)

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