---

Step * 1 of Lemma finite-Ramsey


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)) ∈ ℤ
BY
{ (RWO "8" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  n  :  \mBbbN{}
3.  N  :  \mBbbN{}\msupplus{}
4.  g  :  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}k
5.  i  :  \mBbbN{}k
6.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}N
7.  Inj(\mBbbN{}n;\mBbbN{}N;f)
8.  \mforall{}a,b:\mBbbN{}n.    (f  a  <  f  b  {}\mRightarrow{}  ((g  (f  a)  (f  b))  =  i))
9.  Inj(\mBbbN{}n;\mBbbN{}N;f)
10.  a  :  \mBbbN{}n
11.  b  :  \mBbbN{}n
12.  c  :  \mBbbN{}n
13.  d  :  \mBbbN{}n
14.  f  a  <  f  b
15.  f  c  <  f  d
\mvdash{}  (g  (f  a)  (f  b))  =  (g  (f  c)  (f  d))


By

---

Latex:
(RWO  "8"  0  THEN  Auto)

---

Home Index