nLab
constant function

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$$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)$$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.

See also constant morphism.

Related concepts

• constant function / locally constant function

• constant sheaf / locally constant sheaf

• constant stack / locally constant stack

• constant ∞-stack / locally constant ∞-stack

• local system