Documentation

TauCeti.Data.Nat.Pairing

Columns of the natural-number pairing function #

For Nat.pair : ℕ → ℕ → ℕ, the e-th column e.pairColumn = {n | n.unpair.2 = e} is Soare's ω^{[e]}. Distinct columns are disjoint with union Set.univ, and Nat.leastInPairColumn e b computes the least element of e.pairColumn ∩ Set.Ici b by bounded search up to Nat.pair b e.

References #

source
def Nat.pairColumn (e : ℕ) :
Set ℕ

The e-th column {n | n.unpair.2 = e} of Nat.pair, consisting of all Nat.pair x e.

Instances For
    source
    @[simp]
    theorem Nat.mem_pairColumn {e n : ℕ} :
    n ∈ e.pairColumn ↔ (unpair n).2 = e

    Membership in e.pairColumn means having second Nat.unpair coordinate e.

    source
    @[instance_reducible]
    instance Nat.instDecidablePredMemPairColumn (e : ℕ) :
    DecidablePred fun (x : ℕ) => x ∈ e.pairColumn

    Membership in e.pairColumn is decidable.

    source
    theorem Nat.pair_mem_pairColumn (x e : ℕ) :
    pair x e ∈ e.pairColumn

    Nat.pair x e belongs to the e-th column.

    source
    theorem Nat.pairColumn_eq_range_pair (e : ℕ) :
    e.pairColumn = Set.range fun (x : ℕ) => pair x e

    The e-th column is the range of x ↦ Nat.pair x e.

    source
    theorem Nat.pair_zero_le_of_mem_pairColumn {e n : ℕ} (h : n ∈ e.pairColumn) :
    pair 0 e ≤ n

    Every member of e.pairColumn is at least Nat.pair 0 e.

    source
    theorem Nat.le_of_mem_pairColumn {e n : ℕ} (h : n ∈ e.pairColumn) :
    e ≤ n

    Every member of e.pairColumn is at least e.

    source
    theorem Nat.disjoint_pairColumn {d e : ℕ} (h : d ≠ e) :
    Disjoint d.pairColumn e.pairColumn

    Distinct columns are disjoint.

    source
    theorem Nat.pairwise_disjoint_pairColumn :
    Pairwise (Function.onFun Disjoint pairColumn)

    The family of pairing columns is pairwise disjoint.

    source
    @[simp]
    theorem Nat.iUnion_pairColumn :
    ⋃ (e : ℕ), e.pairColumn = Set.univ

    Every natural number belongs to its own second-coordinate column.

    source
    theorem Nat.infinite_pairColumn (e : ℕ) :
    e.pairColumn.Infinite

    Every pairing column is infinite.

    source
    def Nat.leastInPairColumn (e b : ℕ) :
    ℕ

    The least member of e.pairColumn at or above b, found by searching up to Nat.pair b e.

    Instances For
      source
      theorem Nat.leastInPairColumn_def (e b : ℕ) :
      e.leastInPairColumn b = (List.find? (fun (x : ℕ) => decide (b ≤ x ∧ (unpair x).2 = e)) (List.range (pair b e + 1))).getD (pair b e)

      Unfolding Nat.leastInPairColumn as a bounded search over List.range (pair b e + 1).

      source
      theorem Nat.le_leastInPairColumn (e b : ℕ) :
      b ≤ e.leastInPairColumn b

      e.leastInPairColumn b is at least b.

      source
      theorem Nat.leastInPairColumn_mem_pairColumn (e b : ℕ) :
      e.leastInPairColumn b ∈ e.pairColumn

      e.leastInPairColumn b belongs to e.pairColumn.

      source
      @[simp]
      theorem Nat.unpair_leastInPairColumn_snd (e b : ℕ) :
      (unpair (e.leastInPairColumn b)).2 = e

      The second Nat.unpair coordinate of e.leastInPairColumn b is e.

      source
      theorem Nat.leastInPairColumn_le_pair (e b : ℕ) :
      e.leastInPairColumn b ≤ pair b e

      e.leastInPairColumn b is at most Nat.pair b e.

      source
      theorem Nat.leastInPairColumn_le {e b n : ℕ} (hb : b ≤ n) (hn : n ∈ e.pairColumn) :
      e.leastInPairColumn b ≤ n

      e.leastInPairColumn b is minimal among members of e.pairColumn at or above b.

      source
      theorem Nat.leastInPairColumn_eq_iff {e b m : ℕ} :
      e.leastInPairColumn b = m ↔ b ≤ m ∧ m ∈ e.pairColumn ∧ ∀ n < m, b ≤ n → n ∉ e.pairColumn

      Characterization of e.leastInPairColumn b as the least member of e.pairColumn above b.

      source
      @[simp]
      theorem Nat.leastInPairColumn_zero (e : ℕ) :
      e.leastInPairColumn 0 = pair 0 e

      The least member of e.pairColumn overall is Nat.pair 0 e.

      source
      theorem Nat.monotone_leastInPairColumn (e : ℕ) :
      Monotone e.leastInPairColumn

      Raising the lower bound raises e.leastInPairColumn.

      source
      theorem Nat.lt_leastInPairColumn_succ (e b : ℕ) :
      b < e.leastInPairColumn (b + 1)

      Searching from b + 1 yields a column member strictly above b.