Theorems · Definition · Lie groups

ContinuousMonoidHom.ofClass

(A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : TopologicalSpace B] →
            (F : Type u_7) →
              [inst_4 : FunLike F A B] → [ContinuousMapClass F A B] → [MonoidHomClass F A B] → F → A →ₜ* B

For f : F where F is a class of continuous monoid hom, this yields an element ContinuousMonoidHom A B.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

0 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

MonoidMonoidTopologicalSpaceTopologicalSpaceFunLikeContinuousMapClassMonoidHomClass