Commit 2025-09-02 14:50 bea02cde

feature(Analysis/LocallyConvex/Bounded): Quasi-complete spaces (#28609) Define a quasi-complete space (Bourbaki, III.8) and prove that in a quasi-complete space:

• isCompact_closure_of_totallyBounded_quasiComplete: the closure of a totally bounded set is compact .
• isCompact_closedAbsConvexHull_of_totallyBounded: the closed absolute convex hull of a totally bounded set is compact . The closure of a totally bounded subset of a complete space is also compact. For a complete space with zero equipped with a scalar multiplication by a seminormed ring, this is a special case of isCompact_closure_of_totallyBounded_quasiComplete, but we also provide isCompact_closure_of_totallyBounded_complete which does not require a zero or a scalar multiplication. (N.B. isCompact_of_totallyBounded_isClosed (TotallyBounded.closure ht) isClosed_closure provides an alternative proof of isCompact_closure_of_totallyBounded_complete.)