Perfect metric spaces and nontrivial normed vector spaces

[lowasser]

We define

• unit vectors
• nonzero vectors
• nontrivial normed vector spaces (defined by the existence of a nonzero vector)
• normalization of nonzero vectors
• perfect metric spaces (every point is an accumulation point)

...and show that a normed vector space is nontrivial if and only if it is perfect as a metric space.

[lowasser]

Builds on #1973 .