mathlib3

16728b30 - feat(topology/homotopy/contractible): a few convenience lemmas (#14710)

feat(topology/homotopy/contractible): a few convenience lemmas (#14710) If `X` and `Y` are homotopy equivalent spaces, then one is contractible if and only if the other one is contractible.