How to symbolically write "there exists at most" For example, an injective function can be defined as
$\forall y \in Y$ there exists at most one $x \, : \, \forall f(x) = y$
How could I represent the bold part of the above expression? For "there exists at least one" we have $\exists$, for "there exists a unique" we have $\exists!$. Is there a symbolic notation for "...at most one"? The classic definition of injective, i.e., $\forall \, a,b\in X, \, f(a) = f(b) \rightarrow a = b$ seems to side-step this, though.
 A: If you will be using it repeatedly, you could invent a notation...
$$
\forall y \in Y\;\exists^{\le 1} x 
$$
Of course you will have to define it, say like this
$$
\exists^{\le 1} x\;\;\Phi(x)\qquad\text{means}\qquad
\forall x_1 \forall x_2 \big(\Phi(x_1) \wedge \Phi(x_2) \longrightarrow x_1=x_2\big)
$$
A: I have never heard of such a symbol, but if you really want to you can write $\exists !\, x \lor \nexists\, x, \,\dots $
However, this is not easily readable and I would not advise its use at all. 
A: 
For example, an injective function can be defined as
$\forall y {\in} Y$ there exists at most one $x : \, f(x) = y$
How could I represent the bold part of the above expression? For
"there exists at least one" we have $\exists$, for "there exists a
unique" we have $\exists!$. Is there a symbolic notation for "...at
most one"? The classic definition of injective, i.e., $\forall \,
> {a,b}\in X, \, f(a) = f(b) \rightarrow a = b$ seems to side-step this,
though.

If you accept a string of symbols in lieu, then how about:
$$\forall y{\in}Y  \; \exists p\;\forall x{\in}X\:\Big(f(x)=y \implies p=x\Big).       $$
