Theorem Filter.totallyBounded_iSup

Modification history

2026-01-13 23:44

Mathlib/Topology/UniformSpace/Cauchy.lean

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

Added Filter.totallyBounded_iSup View on Github →