Theorems · Definition · Lie groups

MulEquiv.toContinuousMulEquiv

{G : Type u} →
  [inst : TopologicalSpace G] →
    {H : Type v} →
      [inst_1 : TopologicalSpace H] →
        [inst_2 : Mul G] → [inst_3 : Mul H] → (e : G ≃* H) → (∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s) → G ≃ₜ* H

A MulEquiv that respects open sets is a ContinuousMulEquiv.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

5 results in Mathlib

Foundations

Depth 19 from the axioms · uses Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceMulMul