:: deftheorem defines element_left_uniformity UNIFORM3:def 12 :
for G being TopaddGroup
for U being a_neighborhood of 0_ G holds element_left_uniformity U = { [x,y] where x, y is Element of G : (- x) + y in U } ;