### Nuprl Lemma : finite-Ramsey1

`∀c:ℕ. ∀s:ℕc ⟶ ℕ.`
`  ∃N:ℕ+`
`   ∀g:ℕN ⟶ ℕN ⟶ ℕc. ∃i:ℕc. ∃f:ℕs i ⟶ ℕN. (Inj(ℕs i;ℕN;f) ∧ (∀a,b:ℕs i.  (f a < f b `` ((g (f a) (f b)) = i ∈ ℤ))))`

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 :  select: `L[n]` cons: `[a / b]` compose: `f o g` int_upper: `{i...}` nequal: `a ≠ b ∈ T ` assert: `↑b` bnot: `¬bb` subtract: `n - m` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` eq_int: `(i =z j)` bfalse: `ff` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` inject: `Inj(A;B;f)` cand: `A c∧ B` true: `True` less_than': `less_than'(a;b)` ge: `i ≥ j ` squash: `↓T` less_than: `a < b` nat_plus: `ℕ+` nat: `ℕ` sq_type: `SQType(T)` guard: `{T}` so_apply: `x[s]` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` or: `P ∨ Q` decidable: `Dec(P)` prop: `ℙ` top: `Top` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` implies: `P `` Q` not: `¬A` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` member: `t ∈ T` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]`
Rules used in proof :  inlFormation_alt inrFormation_alt isectIsType baseApply equalityIsType2 equalityIsType4 universeEquality minusEquality setEquality sqequalBase pointwiseFunctionality equalityElimination closedConclusion equalityIstype equalityIsType3 equalityIsType1 functionExtensionality baseClosed imageMemberEquality addEquality setIsType imageElimination productEquality functionEquality inhabitedIsType functionIsType intEquality cumulativity hypothesis_subsumption promote_hyp productIsType dependent_set_memberEquality_alt applyLambdaEquality equalitySymmetry equalityTransitivity because_Cache instantiate applyEquality unionElimination universeIsType independent_pairFormation sqequalRule voidElimination isect_memberEquality_alt dependent_functionElimination int_eqEquality lambdaEquality_alt dependent_pairFormation_alt independent_functionElimination approximateComputation independent_isectElimination natural_numberEquality hypothesisEquality hypothesis productElimination rename setElimination isectElimination sqequalHypSubstitution extract_by_obid introduction thin cut lambdaFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}c:\mBbbN{}.  \mforall{}s:\mBbbN{}c  {}\mrightarrow{}  \mBbbN{}.
\mexists{}N:\mBbbN{}\msupplus{}
\mforall{}g:\mBbbN{}N  {}\mrightarrow{}  \mBbbN{}N  {}\mrightarrow{}  \mBbbN{}c
\mexists{}i:\mBbbN{}c.  \mexists{}f:\mBbbN{}s  i  {}\mrightarrow{}  \mBbbN{}N.  (Inj(\mBbbN{}s  i;\mBbbN{}N;f)  \mwedge{}  (\mforall{}a,b:\mBbbN{}s  i.    (f  a  <  f  b  {}\mRightarrow{}  ((g  (f  a)  (f  b))  =  i))))

Date html generated: 2019_10_15-AM-10_27_36
Last ObjectModification: 2019_09_26-PM-04_40_18

Theory : continuity

Home Index