Theorems · Definition · Lie groups

ContinuousAddMonoidHom.toContinuousMap

{A : Type u_7} →
  {B : Type u_8} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → (A →ₜ+ B) → C(A, B)

Reinterpret a ContinuousAddMonoidHom as a ContinuousMap.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

10 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

AddMonoidAddMonoidTopologicalSpaceTopologicalSpace