thickening_singleton — Mathlib

English

The open thickening equals the union over points in E of balls of radius δ: thickening δ E = ⋃_{x ∈ E} B(x, δ).

Русский

Открытое уплотнение равно объединению шаров B(x, δ) по x ∈ E.

LaTeX

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

Lean4

@[simp]
theorem thickening_singleton (δ : ℝ) (x : X) : thickening δ ({ x } : Set X) = ball x δ :=
  by
  ext
  simp [mem_thickening_iff]

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