Theorems · Theorem · Lie groups

ContinuousMulEquiv.apply_symm_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) (y : N), e (e.symm y) = y

e.symm is a right inverse of e, written as e (e.symm 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