Theorems · Inductive type · Lie groups

ContinuousMonoidHom

(A : Type u_2) →
  (B : Type u_3) → [Monoid A] → [Monoid B] → [TopologicalSpace A] → [TopologicalSpace B] → Type (max u_2 u_3)

The type of continuous monoid homomorphisms from A to B. When possible, instead of parametrizing results over (f : ContinuousMonoidHom A B), you should parametrize over (F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [MonoidHomClass F A B] (f : F). When you extend this structure, make sure to extend ContinuousMapClass and/or MonoidHomClass, if needed.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

104 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

MonoidMonoidTopologicalSpaceTopologicalSpace