---

Step * of Lemma Ramsey-n-3

∀n:ℕ. ∃N:ℕ+. ∀g:ℕN ⟶ ℕN ⟶ ℕn. ∃i,j,k:ℕN. (i < j ∧ j < k ∧ ((g i j) = (g i k) ∈ ℤ) ∧ ((g i k) = (g j k) ∈ ℤ))
BY
{ ((D 0 THENA Auto)
   THEN (InstLemma `finite-Ramsey` [⌜n⌝;⌜3⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast')
   THEN ExRepD) }

1
1. n : ℕ
2. N : ℕ+
3. g : ℕN ⟶ ℕN ⟶ ℕn
4. f : ℕ3 ⟶ ℕN
5. Inj(ℕ3;ℕN;f)
6. ∀a,b,c,d:ℕ3.  (f a < f b ⇒ f c < f d ⇒ ((g (f a) (f b)) = (g (f c) (f d)) ∈ ℤ))
⊢ ∃i,j,k:ℕN. (i < j ∧ j < k ∧ ((g i j) = (g i k) ∈ ℤ) ∧ ((g i k) = (g j k) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}
    \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}g:\mBbbN{}N  {}\mrightarrow{}  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}n.  \mexists{}i,j,k:\mBbbN{}N.  (i  <  j  \mwedge{}  j  <  k  \mwedge{}  ((g  i  j)  =  (g  i  k))  \mwedge{}  ((g  i  k)  =  (g  j  k)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstLemma  `finite-Ramsey`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}3\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast')
  THEN  ExRepD)

---

Home Index