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
    Instances For
      source
      def Nat.unpair (n : ℕ) :
      ℕ × ℕ

      Unpairing function for the natural numbers.

      Equations
        Instances For
          source
          @[simp]
          theorem Nat.pair_unpair (n : ℕ) :
          pair (unpair n).1 (unpair n).2 = n
          source
          theorem Nat.pair_unpair' {n a b : ℕ} (H : unpair n = (a, b)) :
          pair a b = n
          source
          @[simp]
          theorem Nat.unpair_pair (a b : ℕ) :
          unpair (pair a b) = (a, b)
          source
          def Nat.pairEquiv :
          ℕ × ℕ ≃ ℕ

          An equivalence between ℕ × ℕ and ℕ.

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