A function is a relation $f$ with $(a,b)\in f$ and $(a,c)\in f$ implying $b=c$; $f:A\to B$, the value $f(a)$, domain and codomain

A function is a relation $f$ such that $(a,b)\in f$ and $(a,c)\in f$ imply $b=c$; "relation" is as in Relation, $\mathrm{dom}R$, $\mathrm{ran}R$, $\mathrm{fld}R$, and the specialisations "relation from $A$ to $B$" and "relation on $A$".

For $a\in \mathrm{dom}f$ there is such a $b$, and by the condition just stated there is only one; $f(a)$ denotes that unique $b$, so that $(a,b)\in f$ holds if and only if $a\in \mathrm{dom}f$ and $b=f(a)$ ($(a,b)=(c,d)$ if and only if $a=c$ and $b=d$).

We write $f:A\to B$, and say $f$ is a function from $A$ to $B$, when $f$ is a function with $\mathrm{dom}f=A$ and $\mathrm{ran}f\subseteq B$ (Subset $x\subseteq y$, proper subset $x⊊y$, and the separation notation $\{z\in x:\phi (z)\}$); $A$ is the domain of $f$ and $B$ is a codomain for $f$. Equivalently $f\subseteq A\times B$ with $\mathrm{dom}f=A$ (The Cartesian product $A\times B:=\{z\in \mathcal{P}(\mathcal{P}(A\cup B)):\mathrm{\exists }a\in A\mathrm{\exists }b\in Bz=(a,b)\}$, The Kuratowski ordered pair $(a,b):=\{\{a\},\{a,b\}\}$).

• The codomain belongs to the declaration, not to the set. A function is a set of ordered pairs, and that set determines its domain and its range but not a codomain: the same $f$ satisfies $f:A\to B$ for every $B$ containing $\mathrm{ran}f$. So being onto is a property of the declaration $f:A\to B$ rather than of $f$, while being one-to-one is a property of $f$ alone. This convention is what makes $\mathrm{\varnothing }$ a function $\mathrm{\varnothing }\to B$ for every $B$ at once.

• Total on its domain by construction. There is no partial function here: if $a\mathrm{\notin }\mathrm{dom}f$ then $f(a)$ is not defined, and a function $f:A\to B$ has $\mathrm{dom}f$ equal to $A$ exactly, not merely included in it.