propose better names for the Uniform mixin

[affeldt-aist]

analysis/theories/topology.v

Lines 3788 to 3792 in 0e392b5

	ax1 : Filter entourage ;
	ax2 : forall A, entourage A -> [set xy | xy.1 = xy.2] `<=` A ;
	ax3 : forall A, entourage A -> entourage (A^-1)%classic ;
	ax4 : forall A, entourage A -> exists2 B, entourage B & B \; B `<=` A ;
	ax5 : nbhs = nbhs_ entourage