Ordered pair

An ordered pair is a construction satisfying the fundamental property #m/def/set

(𝑎 1, 𝑏 1) = (𝑎 2, 𝑏 2) ⟺ [𝑎 1 = 𝑎 2] \land [𝑏 1 = 𝑏 2]

the set of all ordered pairs from a given pair of sets forms the cartesian product. One may then define an ordered $𝑛$ -tuple by $(𝑎, 𝑏, 𝑐) = ((𝑎, 𝑏), 𝑐)$ , &c. Compare this with the related universal property of the categorical product.

Construction

Within $Z F$ the typical model, due to Kazimierz Kuratowski, is as follows

(𝑎, 𝑏) = 𝐾 {{𝑎}, {𝑎, 𝑏}}

which satisfies the fundamental property.

#state/develop | #lang/en | #SemBr