Commit 2025-11-14 11:52 3bcc6e8a
View on Github →feat: totally bounded sets have finite covers (#31537)
New result: a totally bounded set has finite ε-covers for all ε > 0.
I then use it to golf and generalize exists_finite_isCover_of_isCompact_closure and exists_finite_isCover_of_isCompact to extended pseudo-metric spaces.