---

Step * of Lemma finite-partition

∀n,k:ℕ. ∀c:ℕn ⟶ ℕk.
  ∃p:ℕk ⟶ (ℕ List)
   ((Σ(||p j|| | j < k) = n ∈ ℤ)
   ∧ (∀j:ℕk. ∀x,y:ℕ||p j||.  p j[x] > p j[y] supposing x < y)
   ∧ (∀j:ℕk. ∀x:ℕ||p j||.  (p j[x] < n c∧ ((c p j[x]) = j ∈ ℤ))))
BY
{ InductionOnNat }

1
.....basecase..... 
∀k:ℕ. ∀c:ℕ0 ⟶ ℕk.
  ∃p:ℕk ⟶ (ℕ List)
   ((Σ(||p j|| | j < k) = 0 ∈ ℤ)
   ∧ (∀j:ℕk. ∀x,y:ℕ||p j||.  p j[x] > p j[y] supposing x < y)
   ∧ (∀j:ℕk. ∀x:ℕ||p j||.  (p j[x] < 0 c∧ ((c p j[x]) = j ∈ ℤ))))

2
.....upcase..... 
1. n : ℤ
2. [%1] : 0 < n
3. ∀k:ℕ. ∀c:ℕn - 1 ⟶ ℕk.
     ∃p:ℕk ⟶ (ℕ List)
      ((Σ(||p j|| | j < k) = (n - 1) ∈ ℤ)
      ∧ (∀j:ℕk. ∀x,y:ℕ||p j||.  p j[x] > p j[y] supposing x < y)
      ∧ (∀j:ℕk. ∀x:ℕ||p j||.  (p j[x] < n - 1 c∧ ((c p j[x]) = j ∈ ℤ))))
⊢ ∀k:ℕ. ∀c:ℕn ⟶ ℕk.
    ∃p:ℕk ⟶ (ℕ List)
     ((Σ(||p j|| | j < k) = n ∈ ℤ)
     ∧ (∀j:ℕk. ∀x,y:ℕ||p j||.  p j[x] > p j[y] supposing x < y)
     ∧ (∀j:ℕk. ∀x:ℕ||p j||.  (p j[x] < n c∧ ((c p j[x]) = j ∈ ℤ))))

---

Latex:

---

Latex:
\mforall{}n,k:\mBbbN{}.  \mforall{}c:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}k.
    \mexists{}p:\mBbbN{}k  {}\mrightarrow{}  (\mBbbN{}  List)
      ((\mSigma{}(||p  j||  |  j  <  k)  =  n)
      \mwedge{}  (\mforall{}j:\mBbbN{}k.  \mforall{}x,y:\mBbbN{}||p  j||.    p  j[x]  >  p  j[y]  supposing  x  <  y)
      \mwedge{}  (\mforall{}j:\mBbbN{}k.  \mforall{}x:\mBbbN{}||p  j||.    (p  j[x]  <  n  c\mwedge{}  ((c  p  j[x])  =  j))))


By

---

Latex:
InductionOnNat

---

Home Index