Definition·D012
Relation
A set of ordered pairs; a way for elements of one set to be related to another.
A relation on
is a relation from
to
. One writes
for
. The domain and range of
are
and
.
In words
R is a relation from A to B exactly when R is a subset of the cartesian product of A and B: the set of exactly those ordered pairs it relates. The domain of R collects the first coordinates a that R relates to some b, and the range collects the second coordinates b that some a is related to.
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
Identifying a relation with its set of pairs (its graph) is the standard extensional move: a relation is what it relates, nothing more. Subsets of products exist whenever the product does, and domain and range are Separation subsets of
and
. Examples throughout the library: the order on the naturals, equivalence relations, and functions, which are just relations with a uniqueness property.