closedBall_subset_cthickening_singleton

English

For any x and δ, closedBall x δ ⊆ cthickening δ {x}.

Русский

Для любого x и δ: closedBall x δ ⊆ cthickening δ {x}.

LaTeX

$$$ closedBall x δ \subseteq cthickening δ \{x\} $$$

Lean4

theorem closedBall_subset_cthickening_singleton {α : Type*} [PseudoMetricSpace α] (x : α) (δ : ℝ) :
    closedBall x δ ⊆ cthickening δ ({ x } : Set α) :=
  by
  rcases lt_or_ge δ 0 with (hδ | hδ)
  · simp only [closedBall_eq_empty.mpr hδ, empty_subset]
  · simp only [cthickening_singleton x hδ, Subset.rfl]

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