### Nuprl 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)) ∈ ℤ))))`

Proof

Definitions occuring in Statement :  inject: `Inj(A;B;f)` int_seg: `{i..j-}` nat_plus: `ℕ+` nat: `ℕ` less_than: `a < b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat: `ℕ` exists: `∃x:A. B[x]` and: `P ∧ Q` cand: `A c∧ B` implies: `P `` Q` prop: `ℙ` subtype_rel: `A ⊆r B` int_seg: `{i..j-}` nat_plus: `ℕ+` so_lambda: `λ2x.t[x]` so_apply: `x[s]` squash: `↓T` true: `True` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  finite-Ramsey1 int_seg_wf less_than_wf inject_wf all_wf equal_wf exists_wf nat_wf squash_wf true_wf iff_weakening_equal
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality lambdaEquality isectElimination natural_numberEquality setElimination rename productElimination dependent_pairFormation sqequalRule independent_pairFormation applyEquality functionExtensionality because_Cache productEquality functionEquality intEquality imageElimination equalityTransitivity equalitySymmetry universeEquality independent_functionElimination imageMemberEquality baseClosed independent_isectElimination

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))))))

Date html generated: 2017_04_20-AM-07_26_05
Last ObjectModification: 2017_02_27-PM-05_59_29

Theory : continuity

Home Index