# Naturals pairing function #

This file defines a pairing function for the naturals as follows:

 0  1  4  9 16
2  3  5 10 17
6  7  8 11 18
12 13 14 15 19
20 21 22 23 24


It has the advantage of being monotone in both directions and sending ⟦0, n^2 - 1⟧ to ⟦0, n - 1⟧².

def Nat.pair (a : ) (b : ) :

Pairing function for the natural numbers.

Equations
• a.pair b = if a < b then b * b + a else a * a + a + b
Instances For
def Nat.unpair (n : ) :

Unpairing function for the natural numbers.

Equations
• n.unpair = let s := n.sqrt; if n - s * s < s then (n - s * s, s) else (s, n - s * s - s)
Instances For
@[simp]
theorem Nat.pair_unpair (n : ) :
n.unpair.1.pair n.unpair.2 = n
theorem Nat.pair_unpair' {n : } {a : } {b : } (H : n.unpair = (a, b)) :
a.pair b = n
@[simp]
theorem Nat.unpair_pair (a : ) (b : ) :
(a.pair b).unpair = (a, b)
@[simp]

An equivalence between ℕ × ℕ and ℕ.

Equations
Instances For
@[simp]
theorem Nat.pair_eq_pair {a : } {b : } {c : } {d : } :
a.pair b = c.pair d a = c b = d
theorem Nat.unpair_lt {n : } (n1 : 1 n) :
n.unpair.1 < n
@[simp]
theorem Nat.unpair_zero :
= 0
theorem Nat.unpair_left_le (n : ) :
n.unpair.1 n
theorem Nat.left_le_pair (a : ) (b : ) :
a a.pair b
theorem Nat.right_le_pair (a : ) (b : ) :
b a.pair b
theorem Nat.unpair_right_le (n : ) :
n.unpair.2 n
theorem Nat.pair_lt_pair_left {a₁ : } {a₂ : } (b : ) (h : a₁ < a₂) :
a₁.pair b < a₂.pair b
theorem Nat.pair_lt_pair_right (a : ) {b₁ : } {b₂ : } (h : b₁ < b₂) :
a.pair b₁ < a.pair b₂
theorem Nat.pair_lt_max_add_one_sq (m : ) (n : ) :
m.pair n < (max m n + 1) ^ 2
theorem Nat.max_sq_add_min_le_pair (m : ) (n : ) :
max m n ^ 2 + min m n m.pair n
theorem Nat.add_le_pair (m : ) (n : ) :
m + n m.pair n
theorem Nat.unpair_add_le (n : ) :
n.unpair.1 + n.unpair.2 n
theorem iSup_unpair {α : Type u_1} [] (f : α) :
⨆ (n : ), f n.unpair.1 n.unpair.2 = ⨆ (i : ), ⨆ (j : ), f i j
theorem iInf_unpair {α : Type u_1} [] (f : α) :
⨅ (n : ), f n.unpair.1 n.unpair.2 = ⨅ (i : ), ⨅ (j : ), f i j
theorem Set.iUnion_unpair_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
⋃ (n : ), s n.unpair.1 ×ˢ t n.unpair.2 = (⋃ (n : ), s n) ×ˢ ⋃ (n : ), t n
theorem Set.iUnion_unpair {α : Type u_1} (f : Set α) :
⋃ (n : ), f n.unpair.1 n.unpair.2 = ⋃ (i : ), ⋃ (j : ), f i j
theorem Set.iInter_unpair {α : Type u_1} (f : Set α) :
⋂ (n : ), f n.unpair.1 n.unpair.2 = ⋂ (i : ), ⋂ (j : ), f i j