Theorem Filter.totallyBounded_comap

Modification history

2026-01-13 23:44

Mathlib/Topology/UniformSpace/UniformEmbedding.lean

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

Added Filter.totallyBounded_comap View on Github →