Theorems · Definition · Lie groups

ContinuousAddMonoidHom.toContinuousAddMonoidHom

{A : Type u_2} →
  {B : Type u_3} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            {F : Type u_7} →
              [inst_4 : FunLike F A B] → [AddMonoidHomClass F A B] → [ContinuousMapClass F A B] → F → A →ₜ+ B

Turn an element of a type F satisfying AddMonoidHomClass F A B and ContinuousMapClass F A B into a ContinuousAddMonoidHom. This is declared as the default coercion from F to ContinuousAddMonoidHom A B.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

14 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

AddMonoidAddMonoidTopologicalSpaceTopologicalSpaceFunLikeAddMonoidHomClassContinuousMapClass