Theorems · Theorem · Lie groups

Filter.Tendsto.conj_nhds_one

∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β]
  {ι : Type u_3} {l : Filter ι} {x : ι → β},
  Filter.Tendsto x l (nhds 1) → ∀ (g : ι → β), Filter.Tendsto (g * x * g⁻¹) l (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 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceGroupIsLeftUniformGroupIsRightUniformGroup