Theorems · Definition · Lie groups

ContinuousMulEquiv.toHomeomorph

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

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

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

8 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceMulMul