mathlib3

af5c778c - feat(topology/[continuous_function, path_connected]): add bundled versions of prod_mk and prod_map (#10512)

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).