nLab
constant function

Contents

Definition

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.

Revised on August 20, 2013 06:51:06 by Mike Shulman (107.194.22.192)