mathlib documentation

data.nat.pairing

def nat.mkpair (a b : ℕ) :

Pairing function for the natural numbers.

Equations

a.mkpair b = ite (a < b) (b * b + a) (a * a + a + b)

def nat.unpair (n : ℕ) :

Unpairing function for the natural numbers.

Equations

n.unpair = let s : ℕ := nat.sqrt n in ite (n - s * s < s) (n - s * s, s) (s, n - s * s - s)

@[simp]

theorem nat.mkpair_unpair (n : ℕ) :

n.unpair.fst.mkpair n.unpair.snd = n

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

a.mkpair b = n

@[simp]

theorem nat.unpair_mkpair (a b : ℕ) :

(a.mkpair b).unpair = (a, b)

theorem nat.surjective_unpair :

function.surjective nat.unpair

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

n.unpair.fst < n

theorem nat.unpair_le_left (n : ℕ) :

n.unpair.fst ≤ n

theorem nat.le_mkpair_left (a b : ℕ) :

a ≤ a.mkpair b

theorem nat.le_mkpair_right (a b : ℕ) :

b ≤ a.mkpair b

theorem nat.unpair_le_right (n : ℕ) :

n.unpair.snd ≤ n

theorem nat.mkpair_lt_mkpair_left {a₁ a₂ : ℕ} (b : ℕ) (h : a₁ < a₂) :

a₁.mkpair b < a₂.mkpair b

theorem nat.mkpair_lt_mkpair_right (a : ℕ) {b₁ b₂ : ℕ} (h : b₁ < b₂) :

a.mkpair b₁ < a.mkpair b₂

theorem set.Union_unpair_prod {α : Type u_1} {β : Type u_2} {s : ℕ → set α} {t : ℕ → set β} :

(⋃ (n : ℕ), (s n.unpair.fst).prod (t n.unpair.snd)) = (⋃ (n : ℕ), s n).prod (⋃ (n : ℕ), t n)