Theorems · Theorem · Lie groups

comap_addConj_nhds_zero

∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : AddGroup β] [IsLeftUniformAddGroup β] [IsRightUniformAddGroup β],
  Filter.comap (fun gx => gx.1 + gx.2 + -gx.1) (nhds 0) = Filter.comap Prod.snd (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

1 results in Mathlib

Foundations

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

Assumes

UniformSpaceAddGroupIsLeftUniformAddGroupIsRightUniformAddGroup