A function is a binary relation that is right-unique, i.e. a binary relation $f$ such that for all $x$, $y$, $z\in\dom f$,
\[(z,x)\in f \,\land\, (z,y)\in f \enspace\rimp\enspace x=y.\]
For each $x\in\dom f$, the value of $f$ at $x$, written as $f(x)$, is the unique $y$ such that $(x,y)\in f$. Another notation for $f(x)=y$ is
\[f : x\mapsto y.\]$f$ is onto $Y$ if $\ran f=Y$.
$f$ is from $X$ to $Y$, written
\[f : X\to Y,\]if $\dom f=X$ and $\ran f\subseteq Y$. In this context, $Y$ is called the codomain of $f$.
$f$ is on $X$ if $f:X\to X$.
The set of all functions from $X$ to $Y$ is denoted by
\[\fun(X,Y).\]This is a set:
\[\fun(X,Y) \subseteq \powerset(X\times Y).\]
- Synonym of function: transformation, mapping
- Synonym of codomain: set of destination
An $n$-ary operation on $X$ is a function $*:X^n\to X$.
If $*$ is a binary operation, we write
\[x*y \quad\text{for}\quad *(x,y).\]
Examples.
- $\varnothing$ is a function (the empty function).