Contents

Definition

Given two sets $S$ and $T$ and an element $x$ of $T$, the constant function from $S$ to $T$ with value $x$ is the function $f$ defined by

$f(a) = x$

for every element $a$ of $S$.

More generally, any function $f: S \to T$ is a constant function if

$f(a) = f(b)$

for every element $a$ and element $b$ of $S$. Note that every constant function with particular value (as defined earlier) is constant (as defined here).

The converse is a little more complicated. If $S$ is inhabited, then every constant function from $S$ to $T$ is the constant function from $S$ to $T$ with some particular value, which is unique. If $S$ is empty but $T$ is inhabited, then the unique function from $S$ to $T$ is constant with any particular value in $T$. If $S$ and $T$ are both empty, then the unique function from $S$ to $T$ is constant, but not constant at any particular value.

Using excluded middle, we can say that, if $T$ is inhabited, then any constant function from $S$ to $T$ is constant at some (possibly not unique) value, but this theorem fails in constructive mathematics.