Theorems · Theorem · Lie groups

comap_conj_nhds_one

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

1 results in Mathlib

Foundations

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

Assumes

UniformSpaceGroupIsLeftUniformGroupIsRightUniformGroup