nLab constant function

Definition

Given two sets $S$ and $T$, there is a function $c:T \to (S \to T)$ such that for every element $x:T$ there is a function $c(x):S \to T$ such that for every element $a:S$, $c(x)(a) = x$. For every element $x:T$, the function $c(x)$ is called the constant function from $S$ to $T$ with value $x$.

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.

See also constant morphism.

Related concepts

• constant of a theory

• constant function / locally constant function

• constant sheaf / locally constant sheaf

• constant stack / locally constant stack

• constant ∞-stack / locally constant ∞-stack

• local system

• weakly constant function

• deterministic random variable, almost surely