### Nuprl Lemma : pigeon-hole-implies-ext

`∀n:ℕ. ∀[m:ℕ]. ∀f:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕi [((f i) = (f j) ∈ ℤ)]) supposing m < n`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` less_than: `a < b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` exists: `∃x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  member: `t ∈ T` int_seg_decide: `int_seg_decide(d;i;j)` it: `⋅` genrec-ap: genrec-ap pi1: `fst(t)` pigeon-hole-implies decidable__exists_int_seg decidable__equal_int any: `any x` decidable__int_equal uall: `∀[x:A]. B[x]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` so_apply: `x[s1;s2;s3;s4]` so_lambda: `λ2x y.t[x; y]` top: `Top` so_apply: `x[s1;s2]` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  pigeon-hole-implies lifting-strict-decide strict4-spread lifting-strict-callbyvalue strict4-decide lifting-strict-int_eq decidable__exists_int_seg decidable__equal_int decidable__int_equal
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry isectElimination baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}[m:\mBbbN{}].  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}m.  \mexists{}i:\mBbbN{}n.  (\mexists{}j:\mBbbN{}i  [((f  i)  =  (f  j))])  supposing  m  <  n

Date html generated: 2018_05_21-PM-00_38_56
Last ObjectModification: 2018_05_18-AM-08_16_16

Theory : list_1

Home Index