Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-03 17:40 5cf34f8f

View on Github →

feat(topology/algebra/continuous_monoid_hom): Continuity of composition (#16319) This PR adds some API regarding continuity of compositions of continuous_monoid_homs.

Estimated changes

Modified src/topology/algebra/continuous_monoid_hom.lean

added theorem continuous_monoid_hom.closed_embedding_to_continuous_map

added def continuous_monoid_hom.comp_left

added def continuous_monoid_hom.comp_right

added theorem continuous_monoid_hom.continuous_comp

added theorem continuous_monoid_hom.continuous_comp_left

added theorem continuous_monoid_hom.continuous_comp_right

added theorem continuous_monoid_hom.continuous_of_continuous_uncurry

added theorem continuous_monoid_hom.embedding_to_continuous_map

modified theorem continuous_monoid_hom.ext

added theorem continuous_monoid_hom.inducing_to_continuous_map

deleted theorem continuous_monoid_hom.is_closed_embedding

deleted theorem continuous_monoid_hom.is_embedding

deleted theorem continuous_monoid_hom.is_inducing

added theorem pontryagin_dual.map_apply

added theorem pontryagin_dual.map_comp

added theorem pontryagin_dual.map_mul

added theorem pontryagin_dual.map_one