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 : ℕ) :
nat.mkpair (nat.unpair n).fst (nat.unpair n).snd = n
source
theorem nat.mkpair_unpair' {n a b : ℕ} (H : nat.unpair n = (a, b)) :
nat.mkpair a b = n
source
@[simp]
theorem nat.unpair_mkpair (a b : ℕ) :
nat.unpair (nat.mkpair a b) = (a, b)
source
def nat.mkpair_equiv  :
ℕ × ℕ ≃ ℕ

An equivalence between ℕ × ℕ and ℕ.

Equations
source
@[simp]
theorem nat.mkpair_equiv_symm_apply  :
⇑(nat.mkpair_equiv.symm) = nat.unpair
source
@[simp]
theorem nat.mkpair_equiv_apply  :
⇑nat.mkpair_equiv = function.uncurry nat.mkpair
source
theorem nat.surjective_unpair  :
function.surjective nat.unpair
source
@[simp]
theorem nat.mkpair_eq_mkpair {a b c d : ℕ} :
nat.mkpair a b = nat.mkpair 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_mkpair (a b : ℕ) :
a ≤ nat.mkpair a b
source
theorem nat.right_le_mkpair (a b : ℕ) :
b ≤ nat.mkpair a b
source
theorem nat.unpair_right_le (n : ℕ) :
(nat.unpair n).snd ≤ n
source
theorem nat.mkpair_lt_mkpair_left {a₁ a₂ : ℕ} (b : ℕ) (h : a₁ < a₂) :
nat.mkpair a₁ b < nat.mkpair a₂ b
source
theorem nat.mkpair_lt_mkpair_right (a : ℕ) {b₁ b₂ : ℕ} (h : b₁ < b₂) :
nat.mkpair a b₁ < nat.mkpair a b₂
source
theorem supr_unpair {α : Type u_1} [complete_lattice α] (f : ℕ → ℕ → α) :
(⨆ (n : ℕ), f (nat.unpair n).fst (nat.unpair n).snd) = ⨆ (i j : ℕ), f i j
source
theorem infi_unpair {α : Type u_1} [complete_lattice α] (f : ℕ → ℕ → α) :
(⨅ (n : ℕ), f (nat.unpair n).fst (nat.unpair n).snd) = ⨅ (i j : ℕ), f i j
source
theorem set.Union_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.Union_unpair {α : Type u_1} (f : ℕ → ℕ → set α) :
(⋃ (n : ℕ), f (nat.unpair n).fst (nat.unpair n).snd) = ⋃ (i j : ℕ), f i j
source
theorem set.Inter_unpair {α : Type u_1} (f : ℕ → ℕ → set α) :
(⋂ (n : ℕ), f (nat.unpair n).fst (nat.unpair n).snd) = ⋂ (i j : ℕ), f i j