Theorems · Theorem · Lie groups

tendsto_conj_nhds_one

∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β],
  Filter.Tendsto (fun gx => gx.1 * gx.2 * gx.1⁻¹) (Filter.comap Prod.snd (nhds 1)) (nhds 1)

Note: this assumes [IsLeftUniformGroup β] [IsRightUniformGroup β] instead of the more typical (and equivalent) [IsUniformGroup β] because this is used in the proof of said equivalence.

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceGroupIsLeftUniformGroupIsRightUniformGroup