| context | $X,Y$ |
| definiendum | $f\in Y^X $ |
| inclusion | $f\in$ partial function$(X,Y)$ |
| postulate | $\bigcup\pi_1(f)=X $ |
One defines $\mathrm{dom}(f):=\bigcup\pi_1(f)$. The requirement $\mathrm{dom}(f)=X$ just says that the function must make sense for all inputs.
Notice that for $f\in Y^X$ and $Y\subset Z$ we also have $f\subset Z^X$. In any situation in which a target set is of relevance, when a function gets introduced one must include a codomain declaration by writing
| $ f\in Y^X \land \mathrm{codom}(f)=Y $ |
|---|
where $\mathrm{codom}$ is a new logical operator. We write the above as
| $ f:X\to Y $ |
|---|
We define following two properties
| predicate | $f\dots \text{functional} \equiv \exists X,Y.\ f\in Y^X$ |
| predicate | $f\dots \text{function} \equiv \exists X,Y.\ f: X\to Y$ |
One must stress that declaring $\text{codom}(f)=Y$ created a context and it does not follow from $f\in Y^X$ itself. The set $\mathrm{im}(f)$ is clearly the smallest codomain, but any set containing $\mathrm{im}(f)$ might be a candidate. Notice for example that the notion of surjectivity of a function totally depends on this so called type declaration. Functions with different codomains still have the same extensional input-output properties, although, formally, one should differentiate between them. E.g. with different function symbols etc. According to the function property, we want to use the term “function” for a set for which we have declared the codomain.
(Alternatively to the above definitions, one could, in the Bourbakian tradition, also define functions to be a triple $\langle X,Y,f\rangle$, which contains not only the graph but also explicitly names a codomain. In this case, the difference of two functions which different codomains can not be overlooked.)
We will introduce concise notation mirroring the concepts of depended types in type theory.
Consider a function $F$ with domain $A$. We write
| predicate | $f:{\large\prod}_{x\in A}F(x)\equiv \left(f:A\to\bigcup_{x\in A} F(x)\right) \land \left(\forall x.\,f(x)\in F(x)\right)$ |
If you think of $F(x)$ as fibers over a point $x\in A$, then $f$ is a section.
If $\{\langle x,y\rangle\}\in f$, we write $y$ as $f(x)$. The set of all pairs $\{\langle x,f(x)\rangle\}$ is also called the graph of the function and here it's formally the same as $f$. The left and right hand side are denoted argument and value. If $a\in A, b\in B$ and $\mathrm{dom}(f)=A\times B$, then $\langle \langle a,b\rangle,f(\langle a,b\rangle)\rangle \in f$ and we usually write $f(a,b)\equiv f(\langle a,b\rangle)$.
Moreover, one often speaks of a family of indexed objects, which is just an index to image prescription, i.e. it's really just a function. This is e.g. written $f=(f_x)_{x\in X}$ while depending on the context different use of symbols are common. E.g. $(X_i)_{i\in I}$, or what is also common is $(a_n)_{n\in \mathbb N}$. The latter is btw. bijective to an infinite sequence.