compactSpace — Mathlib

English

In a proper space, the sphere viewed as a subspace is compact.

Русский

В правильном пространстве сфера, рассматриваемая как подпространство, компактна.

LaTeX

$$$\text{CompactSpace}(\mathrm{sphere}(x,r)).\mathrm{Elem}$$$

Lean4

/-- In a proper pseudometric space, any sphere is a `CompactSpace` when considered as a subtype. -/
instance compactSpace {α : Type*} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : CompactSpace (sphere x r) :=
  isCompact_iff_compactSpace.mp (isCompact_sphere _ _)

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