mathlib documentation

data.nat.pairing

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.mkpair (a b : ℕ) :
ℕ

Pairing function for the natural numbers.

Equations
source
def nat.unpair (n : ℕ) :
ℕ × ℕ

Unpairing function for the natural numbers.

Equations
source
@[simp]
theorem nat.mkpair_unpair (n : ℕ) :
n.unpair.fst.mkpair n.unpair.snd = n
source
theorem nat.mkpair_unpair' {n a b : ℕ} (H : n.unpair = (a, b)) :
a.mkpair b = n
source
@[simp]
theorem nat.unpair_mkpair (a b : ℕ) :
(a.mkpair b).unpair = (a, b)
source
theorem nat.surjective_unpair  :
function.surjective nat.unpair
source
theorem nat.unpair_lt {n : ℕ} (n1 : 1 ≤ n) :
n.unpair.fst < n
source
@[simp]
theorem nat.unpair_zero  :
0.unpair = 0
source
theorem nat.unpair_left_le (n : ℕ) :
n.unpair.fst ≤ n
source
theorem nat.left_le_mkpair (a b : ℕ) :
a ≤ a.mkpair b
source
theorem nat.right_le_mkpair (a b : ℕ) :
b ≤ a.mkpair b
source
theorem nat.unpair_right_le (n : ℕ) :
n.unpair.snd ≤ n
source
theorem nat.mkpair_lt_mkpair_left {a₁ a₂ : ℕ} (b : ℕ) (h : a₁ < a₂) :
a₁.mkpair b < a₂.mkpair b
source
theorem nat.mkpair_lt_mkpair_right (a : ℕ) {b₁ b₂ : ℕ} (h : b₁ < b₂) :
a.mkpair b₁ < a.mkpair b₂
source
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)