Definition·D036
Restriction of a function
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 (computed from the citation graph, not asserted).
Remarks
Exists by Separation as a subset of
. It is a function on
: 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.
Used by
Propose an edit1 published revision