Commit 2021-11-30 13:24 af5c778c

feat(topology/[continuous_function, path_connected]): add bundled versions of prod_mk and prod_map (#10512) I also added a definition for pointwise addition of paths, but I'm not sure it would be really useful in general (my use case is the Sphere eversion project, where I need to add together two paths living in complement subspaces of a real TVS).