Enderton.Set.OrderedPair

A representation of an ordered pair in basic set theory. Like Set, it is assumed an ordered pair is homogeneous.

def OrderedPair {α : Type u_1} (x : α) (y : α) : Set (Set α)

Kazimierz Kuratowski's definition of an ordered pair.

Equations

• OrderedPair x y = {{x}, {x, y}}

theorem OrderedPair.ext_iff {α : Type u_1} {x : α} {y : α} {u : α} {v : α} : OrderedPair x y = OrderedPair u v ↔ x = u ∧ y = v

For any sets x, y, u, and v, ⟨u, v⟩ = ⟨x, y⟩ iff u = x ∧ v = y.