Ordered Pair

(<,> x y) represents an ordered pair of numbers. Each ordered pair maps to a single number. The first number in the pair can be obtained from using the head operation. The second number can be extracted using the tail operation.

Definition

The ordered pair (<,> x y) is defined using triangular numbers:

(= (<,> A B) (+ (tri (+ A B)) A)) /edit/peano/peano_thms.gh/df-op

This formula basically counts every space on a 2D grid, by traveling along the diagonals in the following sequence where each column is a new value of x and each row is a new value of y starting with 0. The triangular numbers form the first column.

Continuing to count in this fashion along the diagonals gives as a one-to-one correspondence between the ordered pairs and individual numbers.

Every individual number maps to a pair of numbers and that mapping is unique for both the first number and the second number.

Theorems

Tuple Overview

Login to edit