isCompact_sphere — Mathlib

English

In a proper pseudo-metric space, every sphere is compact when viewed as a subtype.

Русский

В правильном псевдометрическом пространстве любая сфера является компактной как подмножество.

LaTeX

$$$\text{isCompact_sphere}(x,r)$$$

Lean4

/-- In a proper pseudometric space, all spheres are compact. -/
theorem isCompact_sphere {α : Type*} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : IsCompact (sphere x r) :=
  (isCompact_closedBall x r).of_isClosed_subset isClosed_sphere sphere_subset_closedBall

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