Theorems · Definition · Lie groups

ContinuousAddEquiv.symm

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

The inverse of a ContinuousAddEquiv.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

25 results in Mathlib

Foundations

Depth 16 from the axioms · uses Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceAddAdd