### Nuprl Lemma : Ramsey-n-3

`∀n:ℕ. ∃N:ℕ+. ∀g:ℕN ⟶ ℕN ⟶ ℕn. ∃i,j,k:ℕN. (i < j ∧ j < k ∧ ((g i j) = (g i k) ∈ ℤ) ∧ ((g i k) = (g j k) ∈ ℤ))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat_plus: `ℕ+` nat: `ℕ` less_than: `a < b` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` 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` nat: `ℕ` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` implies: `P `` Q` prop: `ℙ` uall: `∀[x:A]. B[x]` exists: `∃x:A. B[x]` nat_plus: `ℕ+` cand: `A c∧ B` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` so_apply: `x[s]` inject: `Inj(A;B;f)` guard: `{T}` lelt: `i ≤ j < k` uimplies: `b supposing a` sq_type: `SQType(T)` true: `True` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` less_than: `a < b` squash: `↓T` decidable: `Dec(P)` or: `P ∨ Q`
Lemmas referenced :  finite-Ramsey false_wf le_wf int_seg_wf all_wf exists_wf less_than_wf equal_wf nat_wf int_seg_properties subtype_base_sq int_subtype_base nat_plus_properties nat_properties satisfiable-full-omega-tt intformeq_wf itermConstant_wf int_formula_prop_eq_lemma int_term_value_constant_lemma int_formula_prop_wf lelt_wf decidable__or decidable__lt intformand_wf intformnot_wf intformor_wf intformless_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_or_lemma int_formula_prop_less_lemma int_term_value_var_lemma not_wf nat_plus_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation hypothesis isectElimination productElimination dependent_pairFormation functionEquality setElimination rename because_Cache lambdaEquality productEquality intEquality applyEquality functionExtensionality independent_functionElimination equalityTransitivity equalitySymmetry applyLambdaEquality instantiate cumulativity independent_isectElimination voidElimination promote_hyp isect_memberEquality voidEquality computeAll imageMemberEquality baseClosed unionElimination int_eqEquality imageElimination

Latex:
\mforall{}n:\mBbbN{}
\mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}g:\mBbbN{}N  {}\mrightarrow{}  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}n.  \mexists{}i,j,k:\mBbbN{}N.  (i  <  j  \mwedge{}  j  <  k  \mwedge{}  ((g  i  j)  =  (g  i  k))  \mwedge{}  ((g  i  k)  =  (g  j  k)))

Date html generated: 2017_04_20-AM-07_26_16
Last ObjectModification: 2017_02_27-PM-05_59_59

Theory : continuity

Home Index