notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
for @{'uniform_converge $a $x}.
notation > "a 'uniform_converges' x" non associative with precedence 50
for @{'uniform_converge $a $x}.
interpretation "Uniform convergence" 'uniform_converge s u =
notation < "a \nbsp (\u \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 50
for @{'uniform_converge $a $x}.
notation > "a 'uniform_converges' x" non associative with precedence 50
for @{'uniform_converge $a $x}.
interpretation "Uniform convergence" 'uniform_converge s u =