Nuprl Lemma : Veldman-Ramsey

Ramsey's theorem 
     infinite version has 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


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:  Q universe: Type
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] implies:  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: 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

\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