Theorems · Definition · Lie groups

ContinuousMulEquiv.trans

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

The composition of two ContinuousMulEquiv.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

7 results in Mathlib

Foundations

Depth 21 from the axioms · uses Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceMulMulMulTopologicalSpace