---

Step * of Lemma finite-Ramsey

∀k,n:ℕ.
  ∃N:ℕ+
   ∀g:ℕN ⟶ ℕN ⟶ ℕk
     ∃f:ℕn ⟶ ℕN. (Inj(ℕn;ℕN;f) ∧ (∀a,b,c,d:ℕn.  (f a < f b ⇒ f c < f d ⇒ ((g (f a) (f b)) = (g (f c) (f d)) ∈ ℤ))))
BY
{ (InstLemma `finite-Ramsey1` []
   THEN ParallelLast'
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜λi.n⌝  THENA Auto)
   THEN ParallelLast
   THEN ParallelLast'
   THEN Reduce -1
   THEN ExRepD
   THEN D 0 With ⌜f⌝ 
   THEN Auto) }

1
1. k : ℕ
2. n : ℕ
3. N : ℕ+
4. g : ℕN ⟶ ℕN ⟶ ℕk
5. i : ℕk
6. f : ℕn ⟶ ℕN
7. Inj(ℕn;ℕN;f)
8. ∀a,b:ℕn.  (f a < f b ⇒ ((g (f a) (f b)) = i ∈ ℤ))
9. Inj(ℕn;ℕN;f)
10. a : ℕn
11. b : ℕn
12. c : ℕn
13. d : ℕn
14. f a < f b
15. f c < f d
⊢ (g (f a) (f b)) = (g (f c) (f d)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}k,n:\mBbbN{}.
    \mexists{}N:\mBbbN{}\msupplus{}
      \mforall{}g:\mBbbN{}N  {}\mrightarrow{}  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}k
          \mexists{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}N
            (Inj(\mBbbN{}n;\mBbbN{}N;f)
            \mwedge{}  (\mforall{}a,b,c,d:\mBbbN{}n.    (f  a  <  f  b  {}\mRightarrow{}  f  c  <  f  d  {}\mRightarrow{}  ((g  (f  a)  (f  b))  =  (g  (f  c)  (f  d))))))


By

---

Latex:
(InstLemma  `finite-Ramsey1`  []
  THEN  ParallelLast'
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}\mlambda{}i.n\mkleeneclose{}    THENA  Auto)
  THEN  ParallelLast
  THEN  ParallelLast'
  THEN  Reduce  -1
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}f\mkleeneclose{} 
  THEN  Auto)

---

Home Index