Mathlib v3 is deprecated. Go to Mathlib v4

Theorem complete_of_compact_set

Modification history

2019-01-02 10:12
analysis/topology/uniform_space.lean
feat(analysis/topology): complete sets, minor modifications (#557)
Deleted complete_of_compact_setView on Github →
2018-11-05 09:39
analysis/topology/uniform_space.lean
feat(analysis/metric_spaces): Compact and proper spaces (#430)
Added complete_of_compact_setView on Github →