Function

Definition 1. 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 a set $Y$ if $\im f = Y$.

$f$ is from a set $X$ to a set $Y$, written

\[f : X \to Y,\]

if $\dom f = X$ and $\im f \subseteq Y$. In this context, $Y$ is called the codomain of $f$.

$f$ is on a set $X$ if $f : X \to X$.

The set of all functions from a set $X$ to a set $Y$ is denoted by

\[\fun(X, Y).\]

This is a set by Separation Schema:

\[\fun(X, Y) \subseteq \rel(X, Y).\]

Definition 2. An $n$-ary operation on a set $X$ ($n \geq 1$) is a function $* : X^n \to X$.

If $*$ is a binary operation, for each $(x, y) \in \dom {*}$, we write $x * y$ for the value of $*$ at $(x, y)$.