Theorem TotallyBounded.isCompact_of_isComplete

Modification history

2025-09-02 14:50
Mathlib/Topology/UniformSpace/Cauchy.lean
feature(Analysis/LocallyConvex/Bounded): Quasi-complete spaces (#28609) …
Added TotallyBounded.isCompact_of_isCompleteView on Github →