thickening_eq_biUnion_ball — Mathlib

English

The open thickening equals the union of balls over all x ∈ E; precisely, thickening δ E = ⋃ x∈E ball x δ.

Русский

Открытое уплотнение равно объединению шаров над всеми x ∈ E: thickening δ E = ⋃ x∈E ball x δ.

LaTeX

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

Lean4

/-- The (open) `δ`-thickening `Metric.thickening δ E` of a subset `E` in a metric space equals the
union of balls of radius `δ` centered at points of `E`. -/
theorem thickening_eq_biUnion_ball {δ : ℝ} {E : Set X} : thickening δ E = ⋃ x ∈ E, ball x δ :=
  by
  ext x
  simp only [mem_iUnion₂, exists_prop]
  exact mem_thickening_iff

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