Commit 2021-04-11 05:39 fc8e18c1View on Github →
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.
comp_right_continuous_map, the bundled continuous map (for this we need
comp_right_homeomorph, when we precompose by a homeomorphism.
T = Ris a topological ring.
added def continuous_map.comp_right_alg_hom
added theorem continuous_map.comp_right_alg_hom_apply
added theorem continuous_map.comp_right_alg_hom_continuous
added def continuous_map.comp_right_continuous_map
added theorem continuous_map.comp_right_continuous_map_apply
added def continuous_map.comp_right_homeomorph
added theorem continuous_map.dist_lt_of_dist_lt_modulus
added def continuous_map.modulus
added theorem continuous_map.modulus_pos
added theorem continuous_map.norm_coe_le_norm
added theorem continuous_map.uniform_continuity