Theorem isCompact_closure_of_totallyBounded_quasiComplete

Modification history

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