Theorem totallyBounded_empty

Modification history

2024-07-14 15:55

Mathlib/Topology/UniformSpace/Cauchy.lean

feat(UniformSpace/Cauchy): add lemmas about `TotallyBounded` (#13451)

Modified totallyBounded_empty View on Github →

2023-02-03 08:41

Mathlib/Topology/UniformSpace/Cauchy.lean

feat: port Topology.UniformSpace.Cauchy (#2007)

Added totallyBounded_empty View on Github →