nLab value




Value of a variable


Value of a function

In set theory, the value of a function f:XAf \,\colon\, X \longrightarrow A at an element xXx \in X is the element f(x)Af(x) \in A.

More generally, in type theory the value of a function on a term xx of type XX is the term f(x)f(x) of type AA.



Relation to images

The image of a function f:XAf \,\colon\, X \to A on a subset SXS \subset X is the value at SS of the function f *:P(X)P(A)f_\ast \;\colon\; P(X) \to P(A), which in turn is the value at ff of the covariant power set functor P:SetSetP \,\colon\, Set \to Set on the category Set of sets.


See also:

Created on May 8, 2022 at 08:19:51. See the history of this page for a list of all contributions to it.