Given two sets and , there is a function such that for every element there is a function such that for every element , . For every element , the function is called the constant function from to with value .
Given two sets and and an element of , the constant function from to with value is the function defined by
for every element of .
More generally, any function is a constant function if
for every element and element of . Note that every constant function with particular value (as defined earlier) is constant (as defined here).
The converse is a little more complicated. If is inhabited, then every constant function from to is the constant function from to with some particular value, which is unique. If is empty but is inhabited, then the unique function from to is constant with any particular value in . If and are both empty, then the unique function from to is constant, but not constant at any particular value.
Using excluded middle, we can say that, if is inhabited, then any constant function from to 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.