functions | Language en | Definition 1 (id=function.def)

Definition 1 (id=function.def)

A relation ${f}\mathop{\subseteq}{{X}\mathop{\times}{Y}}$ , is called a partial function with domain $X$ (write ${{\mathbf{dom}}}{(}{f}{)}$ ) and codomain $Y$ (write ${{\mathbf{codom}}}{(}{f}{)}$ ), iff for all ${x}\mathrel{\in}{X}$ there is at most one ${y}\mathrel{\in}{Y}$ with ${({x},{y})}\mathrel{\in}{f}$ .

We write $f\colon{X}\mathrel{\rightharpoonup}{Y};{x}\mathrel{\mapsto}{y}$ and ${}{{{f}{(}{x}{)}}\mathrel{=}{y}}{}$ instead of ${({x},{y})}\mathrel{\in}{f}$ . We say that ${f}{(}{x}{)}$ is the application of $f$ to $x$ and call $x$ the argument of $f$ . ${}_{\Box}$

Definition 2 (id=undefined.def)

We call a partial function ${f}\colon{{X}}\mathrel{\rightharpoonup}{Y}$

•

defined at ${x}\mathrel{\in}{X}$ , iff ${({x},{y})}\mathrel{\in}{f}$ for some ${y}\mathrel{\in}{Y}$ and
•

undefined at ${x}\mathrel{\in}{X}$ (write ${}{{{f}{(}{x}{)}}\mathrel{=}{\bot}}{}$ ), iff ${({x},{y})}\mathrel{\not\in}{f}$ for all ${y}\mathrel{\in}{Y}$ .

${}_{\Box}$

Definition 3 (id=total-function.def)

If ${f}\colon{{X}}\mathrel{\rightharpoonup}{Y}$ is a total relation (i.e. for all ${x}\mathrel{\in}{X}$ there is a unique ${y}\mathrel{\in}{Y}$ with ${({x},{y})}\mathrel{\in}{f}$ ), we call $f$ a total function and write ${f}\colon{{X}}\mathrel{\rightarrow}{Y}$ . ${}_{\Box}$

Definition 4

If we do not want to specify whether a partial function is total, then we simply speak of a function. ${}_{\Box}$

Definition 5 (id=funspace.def)

Given sets $A$ and $B$ we will call the set ${{A}}\mathrel{\rightarrow}{B}$ ( ${{A}}\mathrel{\rightharpoonup}{B}$ ) of all (partial) functions from $A$ to $B$ the (partial) function space from $A$ to $B$ . ${}_{\Box}$