Compact_Subspace_of_Metric_Space_is_Bounded

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

compact-spacesmetric-subspacesproofwiki

Let $M = \left({A, d}\right)$ be a metric space. Let $C$ be a subspace of $M$ . If $C$ is compact, then it is bounded.

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

theorem Compact_Subspace_of_Metric_Space_is_Bounded {α : Type _} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) : Bornology.IsBounded s := by sorry

Source

https://proofwiki.org/wiki/Compact_Subspace_of_Metric_Space_is_Bounded

View graph