Axiomatic WikiWWikiDDefinitionsRelation
Definition·D012
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
.
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.
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
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. Its first coordinates form the domain and its second coordinates the range, both Separation subsets, while the declared target
is the codomain. Examples throughout the library: the order on the naturals, equivalence relations, and functions, which are just relations with a uniqueness property.