Theorems · Inductive type · Lie groups

ContinuousAddMonoidHom

(A : Type u_7) →
  (B : Type u_8) → [AddMonoid A] → [AddMonoid B] → [TopologicalSpace A] → [TopologicalSpace B] → Type (max u_7 u_8)

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

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

77 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

AddMonoidAddMonoidTopologicalSpaceTopologicalSpace