metric: define Cauchy sequences, move def of complete metric spaces up. separate out the fact that cauchy sequences with convergent subsequences converge.
metric: more refactoring of the compactness characterization theorem, this time using Lebesgue numbers. The theorem is now proved except for one proposition