Commit 2021-04-11 05:39 fc8e18c1

feat(topology/continuous_function): comp_right_* (#7145) We setup variations on comp_right_* f, where f : C(X, Y) (that is, precomposition by a continuous map), as a morphism C(Y, T) → C(X, T), respecting various types of structure. In particular:

• comp_right_continuous_map, the bundled continuous map (for this we need X Y compact).
• comp_right_homeomorph, when we precompose by a homeomorphism.
• comp_right_alg_hom, when T = R is a topological ring.