mathlib

2a456a9c - feat(topology/*, geometry/*): missing lemmas (#3528)

feat(topology/*, geometry/*): missing lemmas (#3528) Grab bag of missing lemmas on topology and geometry that were needed for the manifold exercises in Lftcm2020. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>