continuous_monoid_hom): Continuity of composition (#16319)

Commit

3 years ago

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

Author

tb65536

Parents

77615d00

mathlib3 5cf34f8f - feat(topology/algebra/continuous_monoid_hom): Continuity of composition (#16319)

mathlib3
5cf34f8f - feat(topology/algebra/continuous_monoid_hom): Continuity of composition (#16319)