Commit 2025-08-23 13:31 43f1506e

View on Github →

chore: generalise the fact that intervals are totally bounded (#28806) UniformSpace is enough, instead of PseudoMetricSpace.

Estimated changes

Modified Mathlib/Topology/MetricSpace/Bounded.lean

modified theorem totallyBounded_Icc

modified theorem totallyBounded_Ico

modified theorem totallyBounded_Ioc

modified theorem totallyBounded_Ioo