### Nuprl Lemma : Veldman-Ramsey

`Ramsey's theorem - `
`     infinite version has a constructive version here⋅`

`∀T:Type. ∀n:ℕ.  ∀[R,S:n-aryRel(T)].  (almost-full(T;n;R) `` almost-full(T;n;S) `` almost-full(T;n;R ∧ S))`

This theorem is one of freek's list of 100 theorems

Proof

Definitions occuring in Statement :  almost-full: `almost-full(T;n;R)` nary-rel: `n-aryRel(T)` prop_and: `P ∧ Q` nat: `ℕ` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` almost-full: `almost-full(T;n;R)` exists: `∃x:A. B[x]` member: `t ∈ T` prop: `ℙ` nat: `ℕ` guard: `{T}` or: `P ∨ Q` prop_and: `P ∧ Q` nary-rel: `n-aryRel(T)` false: `False` and: `P ∧ Q` nary-rel-predicate: `[[R]]` cand: `A c∧ B`
Lemmas referenced :  almost-full_wf nary-rel_wf nat_wf false_wf int_seg_wf tree-secures_functionality nary-rel-predicate_wf or_wf Veldman-Coquand and_wf tree-tensor_wf tree-secures_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation sqequalHypSubstitution productElimination thin cut lemma_by_obid isectElimination hypothesisEquality hypothesis universeEquality lambdaEquality functionEquality natural_numberEquality setElimination rename dependent_functionElimination because_Cache sqequalRule applyEquality independent_functionElimination inrFormation dependent_pairFormation unionElimination voidElimination independent_pairFormation

Latex:
\mforall{}T:Type.  \mforall{}n:\mBbbN{}.
\mforall{}[R,S:n-aryRel(T)].    (almost-full(T;n;R)  {}\mRightarrow{}  almost-full(T;n;S)  {}\mRightarrow{}  almost-full(T;n;R  \mwedge{}  S))

Date html generated: 2016_07_08-PM-04_49_44
Last ObjectModification: 2015_12_26-PM-07_54_56

Theory : fan-theorem

Home Index