instCompactSpaceElemClosedBallOfProperSpace

English

For a proper space, the closed ball is compact as a subset; its elements form a compact space.

Русский

В правильном пространстве замкнутый шар является компактным подпространством; элементы шарa образуют компактное множество.

LaTeX

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

Lean4

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

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