For example, an injective function can be defined as
∀y∈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 ∃, for "there exists a unique" we have ∃!. Is there a symbolic notation for "...at most one"? The classic definition of injective, i.e., ∀a,b∈X,f(a)=f(b)→a=b seems to side-step this, though.
