cthickening_singleton — Mathlib

English

For a fixed x and δ ≥ 0, cthickening δ {x} = closedBall x δ.

Русский

Для фиксированного x и δ ≥ 0 выполняется cthickening δ {x} = closedBall x δ.

LaTeX

$$$ δ \ge 0 \Rightarrow cthickening δ \{x\} = closedBall x δ $$$

Lean4

@[simp]
theorem cthickening_singleton {α : Type*} [PseudoMetricSpace α] (x : α) {δ : ℝ} (hδ : 0 ≤ δ) :
    cthickening δ ({ x } : Set α) = closedBall x δ := by
  ext y
  simp [cthickening, edist_dist, ENNReal.ofReal_le_ofReal_iff hδ]

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