Theorems · Theorem · Lie groups

Filter.Tendsto.addConj_nhds_zero

∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β]
  {ι : Type u_3} {l : Filter ι} {x : ι → β},
  Filter.Tendsto x l (nhds 0) → ∀ (g : ι → β), Filter.Tendsto (g + x + -g) l (nhds 0)

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

Defined in

Mathlib.Topology.Algebra.IsUniformGroup.Defs

Cited by

0 results in Mathlib

Foundations

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

Assumes

UniformSpaceAddGroupIsLeftUniformAddGroupIsRightUniformAddGroup