Theorems · Theorem · Lie groups

ContinuousMulEquiv.symm_apply_apply

∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (e : M ≃ₜ* N) (x : M), e.symm (e x) = x

e.symm is a left inverse of e, written as e.symm (e y) = y.

Defined in

Mathlib.Topology.Algebra.ContinuousMonoidHom

Cited by

2 results in Mathlib

Foundations

Depth 21 from the axioms · uses Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceMulMul