Theorem Filter.totallyBounded_bot

Modification history

2026-01-13 23:44

Mathlib/Topology/UniformSpace/Cauchy.lean

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

Added Filter.totallyBounded_bot View on Github →