Theorems · Definition · Lie groups

ContinuousAddEquiv.toHomeomorph

{G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} → [inst_1 : TopologicalSpace H] → [inst_2 : Add G] → [inst_3 : Add H] → G ≃ₜ+ H → G ≃ₜ H

The homeomorphism induced from a two-sided continuous isomorphism additive groups.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

8 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceAddAdd