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⟧².

source

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

ℕ

Pairing function for the natural numbers.

Equations

Nat.pair a b = if a < b then b * b + a else a * a + a + b

Instances For

source

def Nat.unpair (n : ℕ) :

ℕ × ℕ

Unpairing function for the natural numbers.

Equations

Nat.unpair n = let s := Nat.sqrt n; if n - s * s < s then (n - s * s, s) else (s, n - s * s - s)

Instances For

source

@[simp]

theorem Nat.pair_unpair (n : ℕ) :

Nat.pair (Nat.unpair n).fst (Nat.unpair n).snd = n

source

theorem Nat.pair_unpair' {n : ℕ} {a : ℕ} {b : ℕ} (H : Nat.unpair n = (a, b)) :

Nat.pair a b = n

source

@[simp]

theorem Nat.unpair_pair (a : ℕ) (b : ℕ) :

Nat.unpair (Nat.pair a b) = (a, b)

source

@[simp]

theorem Nat.pairEquiv_symm_apply :

↑Nat.pairEquiv.symm = Nat.unpair

source

@[simp]

theorem Nat.pairEquiv_apply :

↑Nat.pairEquiv = Function.uncurry Nat.pair

source

def Nat.pairEquiv :

ℕ × ℕ ≃ ℕ

An equivalence between ℕ × ℕ and ℕ.

Equations

Nat.pairEquiv = { toFun := Function.uncurry Nat.pair, invFun := Nat.unpair, left_inv := Nat.pairEquiv.proof_1, right_inv := Nat.pair_unpair }

Instances For

source

theorem Nat.surjective_unpair :

Function.Surjective Nat.unpair

source

@[simp]

theorem Nat.pair_eq_pair {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} :

Nat.pair a b = Nat.pair c d ↔ a = c ∧ b = d

source

theorem Nat.unpair_lt {n : ℕ} (n1 : 1 ≤ n) :

(Nat.unpair n).fst < n

source

@[simp]

theorem Nat.unpair_zero :

Nat.unpair 0 = 0

source

theorem Nat.unpair_left_le (n : ℕ) :

(Nat.unpair n).fst ≤ n

source

theorem Nat.left_le_pair (a : ℕ) (b : ℕ) :

a ≤ Nat.pair a b

source

theorem Nat.right_le_pair (a : ℕ) (b : ℕ) :

b ≤ Nat.pair a b

source

theorem Nat.unpair_right_le (n : ℕ) :

(Nat.unpair n).snd ≤ n

source

theorem Nat.pair_lt_pair_left {a₁ : ℕ} {a₂ : ℕ} (b : ℕ) (h : a₁ < a₂) :

Nat.pair a₁ b < Nat.pair a₂ b

source

theorem Nat.pair_lt_pair_right (a : ℕ) {b₁ : ℕ} {b₂ : ℕ} (h : b₁ < b₂) :

Nat.pair a b₁ < Nat.pair a b₂

source

theorem Nat.pair_lt_max_add_one_sq (m : ℕ) (n : ℕ) :

Nat.pair m n < (max m n + 1) ^ 2

source

theorem Nat.max_sq_add_min_le_pair (m : ℕ) (n : ℕ) :

max m n ^ 2 + min m n ≤ Nat.pair m n

source

theorem Nat.add_le_pair (m : ℕ) (n : ℕ) :

m + n ≤ Nat.pair m n

source

theorem Nat.unpair_add_le (n : ℕ) :

(Nat.unpair n).fst + (Nat.unpair n).snd ≤ n

source

theorem iSup_unpair {α : Type u_1} [CompleteLattice α] (f : ℕ → ℕ → α) :

⨆ (n : ℕ), f (Nat.unpair n).fst (Nat.unpair n).snd = ⨆ (i : ℕ) (j : ℕ), f i j

source

theorem iInf_unpair {α : Type u_1} [CompleteLattice α] (f : ℕ → ℕ → α) :

⨅ (n : ℕ), f (Nat.unpair n).fst (Nat.unpair n).snd = ⨅ (i : ℕ) (j : ℕ), f i j

source

theorem Set.iUnion_unpair_prod {α : Type u_1} {β : Type u_2} {s : ℕ → Set α} {t : ℕ → Set β} :

⋃ (n : ℕ), s (Nat.unpair n).fst ×ˢ t (Nat.unpair n).snd = (⋃ (n : ℕ), s n) ×ˢ ⋃ (n : ℕ), t n

source

theorem Set.iUnion_unpair {α : Type u_1} (f : ℕ → ℕ → Set α) :

⋃ (n : ℕ), f (Nat.unpair n).fst (Nat.unpair n).snd = ⋃ (i : ℕ) (j : ℕ), f i j

source

theorem Set.iInter_unpair {α : Type u_1} (f : ℕ → ℕ → Set α) :

⋂ (n : ℕ), f (Nat.unpair n).fst (Nat.unpair n).snd = ⋂ (i : ℕ) (j : ℕ), f i j