Theorems · Theorem · Lie groups

IsRightUniformAddGroup.uniformity_eq

∀ {G : Type u_7} {inst : UniformSpace G} {inst_1 : AddGroup G} [self : IsRightUniformAddGroup G],
  uniformity G = Filter.comap (fun x => x.2 + -x.1) (nhds 0)

Defined in: Mathlib.Topology.Algebra.IsUniformGroup.Defs
Cited by: 1 results in Mathlib
Foundations: Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: IsRightUniformAddGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Filterstatement · cited by 8,121
nhdsstatement · cited by 5,554
AddGroupstatement and proof · cited by 4,410
UniformSpacestatement and proof · cited by 2,040
uniformitystatement · cited by 765
Filter.comapstatement · cited by 546
IsRightUniformAddGroupstatement and proof · cited by 9

Cited by1

Results whose statement or proof uses this declaration.

uniformity_eq_comap_add_neg_nhds_zeroproof · cited by 4