Theorems · Theorem · Lie groups

IsTopologicalGroup.continuous_conj_prod

∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Inv G] [inst_2 : Mul G] [ContinuousMul G] [ContinuousInv G],
  Continuous fun g => g.1 * g.2 * g.1⁻¹

Conjugation is jointly continuous on G × G when both mul and inv are continuous.

Defined in

Mathlib.Topology.Algebra.Group.Basic

Cited by

0 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceInvMulContinuousMulContinuousInv