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
for every element $a$ of $S$.
More generally, any function $f: S \to T$ is a constant function if
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.
See also constant morphism.
constant function / locally constant function
Last revised on August 20, 2013 at 06:51:06. See the history of this page for a list of all contributions to it.