Theorem totallyBounded_subset

Modification history

2024-07-14 15:55

Mathlib/Topology/UniformSpace/Cauchy.lean

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

Deleted totallyBounded_subset View on Github →

2023-02-03 08:41

Mathlib/Topology/UniformSpace/Cauchy.lean

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

Added totallyBounded_subset View on Github →