Theorems · Definition · Lie groups

ContinuousAddEquiv.trans

{M : Type u_1} →
  {N : Type u_2} →
    [inst : TopologicalSpace M] →
      [inst_1 : TopologicalSpace N] →
        [inst_2 : Add M] →
          [inst_3 : Add N] →
            {L : Type u_3} → [inst_4 : Add L] → [inst_5 : TopologicalSpace L] → M ≃ₜ+ N → N ≃ₜ+ L → M ≃ₜ+ L

The composition of two ContinuousAddEquiv.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

7 results in Mathlib

Foundations

Depth 21 from the axioms · uses Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceAddAddAddTopologicalSpace