Theorem TotallyBounded.closure

Modification history

2026-01-13 23:44

Mathlib/Topology/UniformSpace/Cauchy.lean

feat(Topology/UniformSpace): generalize `TotallyBounded` to filters (#33128) …

Modified TotallyBounded.closure View on Github →

2023-02-03 08:41

Mathlib/Topology/UniformSpace/Cauchy.lean

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

Added TotallyBounded.closure View on Github →