---

Step * of Lemma Dickson's lemma

∀p:ℕ. ∀A:ℕp ⟶ ℕ ⟶ ℕ.  ∃j:ℕ. ∃i:ℕj. ∀k:ℕp. (A[k;i] ≤ A[k;j])
BY
{ (CompNatInd' THEN Auto)⋅ }

1
1. p : ℕ
2. ∀p1:ℕp. ∀A:ℕp1 ⟶ ℕ ⟶ ℕ.  ∃j:ℕ. ∃i:ℕj. ∀k:ℕp1. (A[k;i] ≤ A[k;j])
3. A : ℕp ⟶ ℕ ⟶ ℕ
⊢ ∃j:ℕ. ∃i:ℕj. ∀k:ℕp. (A[k;i] ≤ A[k;j])

---

Latex:

---

Latex:
\mforall{}p:\mBbbN{}.  \mforall{}A:\mBbbN{}p  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}.    \mexists{}j:\mBbbN{}.  \mexists{}i:\mBbbN{}j.  \mforall{}k:\mBbbN{}p.  (A[k;i]  \mleq{}  A[k;j])


By

---

Latex:
(CompNatInd'  THEN  Auto)\mcdot{}

---

Home Index