Definition·D010
Ordered pair
A pair with a first and a second coordinate, built from unordered pairs.
using the singleton and the unordered pair of D003; the set exists by Pairing applied three times: to form
, to form
, and to gather them into
.
In words
The ordered pair of a and b is the set whose members are the singleton of a and the unordered pair of a and b. Unlike the unordered pair, it remembers which element comes first.
Rests onA02
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Kuratowski's coding. The unordered pair
of D003 satisfies
, so it cannot record order; the asymmetry between
and
in
is exactly what does. That this coding works, meaning that the pair determines its coordinates, is the content of L01. Any other coding with that property would serve equally well: nothing downstream depends on the internal anatomy of
, only on the characteristic property. On this wiki the ordered pair is rendered with angle brackets, keeping tuples visually distinct from the parentheses of grouping and function application; many texts write the same object as (a, b).