# Commit 2018-12-24 20:12 a04c7e20

View on Github →feat(analysis/topology): miscellaneous topology (#484)

- miscellaneous topology
- C is a proper metric space
- Sum of metric spaces is a def instead of instance
- refactor(analysis): shorten/simplify proofs

Mathlib v3 is deprecated. Go to Mathlib v4

feat(analysis/topology): miscellaneous topology (#484)

- miscellaneous topology
- C is a proper metric space
- Sum of metric spaces is a def instead of instance
- refactor(analysis): shorten/simplify proofs