Axiomatic WikiWWikiDDefinitionsRestriction of a function
Definition·D036
The same function, considered only on part of its domain.
In words
The restriction of f to X is the set of pairs of f whose first coordinate lies in 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 · A09 (computed from the citation graph, not asserted).
Remarks
Exists by Separation as a subset of
. It is a function on
, cutting the domain of
down to
: each
has exactly one value under
(D013), and precisely the pairs with first coordinate in
survive (L01). Restrictions of injective functions are injective (fewer arguments, same values), which L24 and L27 exploit; the image of a restriction,
, is the image notation on the smaller domain.