Function
Set
| context | $X,Y$ |
| definiendum | $f\in Y^X $ |
| inclusion | $f\in$ partial function$(X,Y)$ |
| postulate | $\bigcup\pi_1(f)=X $ |
Discussion
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.
Predicates
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.)
Depended functions within set theory
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.
Notation
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.
Parents
Subset of
Element of
Context
Related
