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

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

Pairing function for the natural numbers.

Equations
Instances For
    def Nat.unpair (n : ) :

    Unpairing function for the natural numbers.

    Equations
    • Nat.unpair n = if n - n.sqrt * n.sqrt < n.sqrt then (n - n.sqrt * n.sqrt, n.sqrt) else (n.sqrt, n - n.sqrt * n.sqrt - n.sqrt)
    Instances For
      @[simp]
      theorem Nat.pair_unpair (n : ) :
      theorem Nat.pair_unpair' {n : } {a : } {b : } (H : Nat.unpair n = (a, b)) :
      Nat.pair a b = n
      @[simp]
      theorem Nat.unpair_pair (a : ) (b : ) :
      Nat.unpair (Nat.pair a b) = (a, b)

      An equivalence between ℕ × ℕ and .

      Equations
      Instances For
        @[simp]
        theorem Nat.pair_eq_pair {a : } {b : } {c : } {d : } :
        Nat.pair a b = Nat.pair c d a = c b = d
        theorem Nat.unpair_lt {n : } (n1 : 1 n) :
        (Nat.unpair n).1 < n
        @[simp]
        theorem Nat.left_le_pair (a : ) (b : ) :
        theorem Nat.right_le_pair (a : ) (b : ) :
        theorem Nat.pair_lt_pair_left {a₁ : } {a₂ : } (b : ) (h : a₁ < a₂) :
        Nat.pair a₁ b < Nat.pair a₂ b
        theorem Nat.pair_lt_pair_right (a : ) {b₁ : } {b₂ : } (h : b₁ < b₂) :
        Nat.pair a b₁ < Nat.pair a b₂
        theorem Nat.pair_lt_max_add_one_sq (m : ) (n : ) :
        Nat.pair m n < (max m n + 1) ^ 2
        theorem Nat.max_sq_add_min_le_pair (m : ) (n : ) :
        max m n ^ 2 + min m n Nat.pair m n
        theorem Nat.add_le_pair (m : ) (n : ) :
        m + n Nat.pair m n
        theorem Nat.unpair_add_le (n : ) :
        (Nat.unpair n).1 + (Nat.unpair n).2 n
        theorem iSup_unpair {α : Type u_1} [CompleteLattice α] (f : α) :
        ⨆ (n : ), f (Nat.unpair n).1 (Nat.unpair n).2 = ⨆ (i : ), ⨆ (j : ), f i j
        theorem iInf_unpair {α : Type u_1} [CompleteLattice α] (f : α) :
        ⨅ (n : ), f (Nat.unpair n).1 (Nat.unpair n).2 = ⨅ (i : ), ⨅ (j : ), f i j
        theorem Set.iUnion_unpair_prod {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} :
        ⋃ (n : ), s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2 = (⋃ (n : ), s n) ×ˢ ⋃ (n : ), t n
        theorem Set.iUnion_unpair {α : Type u_1} (f : Set α) :
        ⋃ (n : ), f (Nat.unpair n).1 (Nat.unpair n).2 = ⋃ (i : ), ⋃ (j : ), f i j
        theorem Set.iInter_unpair {α : Type u_1} (f : Set α) :
        ⋂ (n : ), f (Nat.unpair n).1 (Nat.unpair n).2 = ⋂ (i : ), ⋂ (j : ), f i j