n:
. r
n 
(G:({s:(n List)| ||s|| = k 
& (x,y:||s||. x < y s[x] < s[y]) }
||L||). 
c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c))
is mentioned by
Thm* k: , L: List. 0 < ||L|| (r:. r- > L^k) | [Ramsey] |
| Thm* r,k:, L,R: List. 2k ||R|| = ||L|| (i:||L||. 0 < L[i] R[i]- > L[i--]^k) r- > R^k-1 r+1- > L^k | [Ramsey-recursion] |
| Thm* L: List. sum(L[i]-1 | i < ||L||)+1- > L^1 | [Ramsey-base-case] |
| Thm* k:, L: List, r1,r2:. r1r2 r1- > L^k r2- > L^k | [arrows-monotone1] |
Thm* k:, L: List. k-1- > L^k  (i:||L||. L[i] < k) | [trivial-arrows] |
Try larger context:
Graphs