nLab constant function

Contents

Contents

Definition

Given two sets SS and TT, there is a function c:T(ST)c:T \to (S \to T) such that for every element x:Tx:T there is a function c(x):STc(x):S \to T such that for every element a:Sa:S, c(x)(a)=xc(x)(a) = x. For every element x:Tx:T, the function c(x)c(x) is called the constant function from SS to TT with value xx.

Given two sets SS and TT and an element xx of TT, the constant function from SS to TT with value xx is the function ff defined by

f(a)=x f(a) = x

for every element aa of SS.

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

f(a)=f(b) f(a) = f(b)

for every element aa and element bb of SS. Note that every constant function with particular value (as defined earlier) is constant (as defined here).

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

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

See also constant morphism.

Last revised on July 26, 2023 at 19:46:34. See the history of this page for a list of all contributions to it.