Documentation

Mathlib.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.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
    source
    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
      source
      @[simp]
      theorem Nat.pair_unpair (n : ℕ) :
      n.unpair.1.pair n.unpair.2 = n
      source
      theorem Nat.pair_unpair' {n : ℕ} {a : ℕ} {b : ℕ} (H : n.unpair = (a, b)) :
      a.pair b = n
      source
      @[simp]
      theorem Nat.unpair_pair (a : ℕ) (b : ℕ) :
      (a.pair b).unpair = (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
      Instances For
        source
        theorem Nat.surjective_unpair :
        Function.Surjective Nat.unpair
        source
        @[simp]
        theorem Nat.pair_eq_pair {a : ℕ} {b : ℕ} {c : ℕ} {d : ℕ} :
        a.pair b = c.pair d ↔ a = c ∧ b = d
        source
        theorem Nat.unpair_lt {n : ℕ} (n1 : 1 ≤ n) :
        n.unpair.1 < n
        source
        @[simp]
        theorem Nat.unpair_zero :
        Nat.unpair 0 = 0
        source
        theorem Nat.unpair_left_le (n : ℕ) :
        n.unpair.1 ≤ n
        source
        theorem Nat.left_le_pair (a : ℕ) (b : ℕ) :
        a ≤ a.pair b
        source
        theorem Nat.right_le_pair (a : ℕ) (b : ℕ) :
        b ≤ a.pair b
        source
        theorem Nat.unpair_right_le (n : ℕ) :
        n.unpair.2 ≤ n
        source
        theorem Nat.pair_lt_pair_left {a₁ : ℕ} {a₂ : ℕ} (b : ℕ) (h : a₁ < a₂) :
        a₁.pair b < a₂.pair b
        source
        theorem Nat.pair_lt_pair_right (a : ℕ) {b₁ : ℕ} {b₂ : ℕ} (h : b₁ < b₂) :
        a.pair b₁ < a.pair b₂
        source
        theorem Nat.pair_lt_max_add_one_sq (m : ℕ) (n : ℕ) :
        m.pair n < (max m n + 1) ^ 2
        source
        theorem Nat.max_sq_add_min_le_pair (m : ℕ) (n : ℕ) :
        max m n ^ 2 + min m n ≤ m.pair n
        source
        theorem Nat.add_le_pair (m : ℕ) (n : ℕ) :
        m + n ≤ m.pair n
        source
        theorem Nat.unpair_add_le (n : ℕ) :
        n.unpair.1 + n.unpair.2 ≤ n
        source
        theorem iSup_unpair {α : Type u_1} [CompleteLattice α] (f : ℕ → ℕ → α) :
        ⨆ (n : ℕ), f n.unpair.1 n.unpair.2 = ⨆ (i : ℕ), ⨆ (j : ℕ), f i j
        source
        theorem iInf_unpair {α : Type u_1} [CompleteLattice α] (f : ℕ → ℕ → α) :
        ⨅ (n : ℕ), f n.unpair.1 n.unpair.2 = ⨅ (i : ℕ), ⨅ (j : ℕ), f i j
        source
        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
        source
        theorem Set.iUnion_unpair {α : Type u_1} (f : ℕ → ℕ → Set α) :
        ⋃ (n : ℕ), f n.unpair.1 n.unpair.2 = ⋃ (i : ℕ), ⋃ (j : ℕ), f i j
        source
        theorem Set.iInter_unpair {α : Type u_1} (f : ℕ → ℕ → Set α) :
        ⋂ (n : ℕ), f n.unpair.1 n.unpair.2 = ⋂ (i : ℕ), ⋂ (j : ℕ), f i j