Definition·D013
Function
A relation assigning to each element of its domain exactly one value.
For
, the unique
with
is written
.
In words
f is a function from A to B exactly when f is a subset of the cartesian product of A and B and for every x, if x belongs to A then there is exactly one y that f pairs with x. That unique y is written f(x), the value of f at x.
Rests onno axioms yet
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A02 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
A function is its graph: a relation (a subset of the cartesian product
) that is total (every
has a value) and single-valued (at most one value each), the two conditions folded into the unique existence quantifier of Replacement's statement. Note that the target
is not recoverable from the graph alone; "
" is a statement about
,
and
jointly. The image
of a subset
is D007. Functions are the single most used notion downstream: sequences, operations, bijections and group operations are all functions.