Theorems · Definition · Lie groups

ContinuousMulEquiv.symm

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

The inverse of a ContinuousMulEquiv.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

27 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceMulMul