Proper metric space (source code)

= Proper metric space
{wiki}

A metric space is proper when every closed bounded subset is compact.