Totally_Bounded_Metric_Space_is_Bounded

Proved

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

bounded-metric-spacesproofwikitotally-bounded-metric-spaces

Let $M = \struct {A, d}$ be a totally bounded metric space. Then $M$ is bounded.

Preamble

import Mathlib.Topology.MetricSpace.Basic

Formal statement

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

Source

https://proofwiki.org/wiki/Totally_Bounded_Metric_Space_is_Bounded

View graph