Commit 2021-10-04 15:09 387ff6e3

View on Github →

feat(topology/homotopy): add homotopy_with (#9252) Added homotopy_with as in HOL-Analysis extending homotopy. Furthermore, I've added homotopy_rel. Also rename/moved the file. There is also some refactoring which is part of the suggestions from #9141 .

Estimated changes

added structure continuous_map.homotopy