Nuprl Lemma : pigeon-hole-implies

`∀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 :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` uimplies: `b supposing a` member: `t ∈ T` nat: `ℕ` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` lelt: `i ≤ j < k` and: `P ∧ Q` guard: `{T}` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` so_apply: `x[s]` inject: `Inj(A;B;f)` le: `A ≤ B` less_than: `a < b` sq_exists: `∃x:{A| B[x]}`
Lemmas referenced :  member-less_than decidable__exists_int_seg exists_wf int_seg_wf equal_wf int_seg_properties nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_wf lelt_wf decidable__equal_int pigeon-hole less_than_wf nat_wf intformeq_wf int_formula_prop_eq_lemma decidable__le intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma sq_exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis independent_isectElimination instantiate dependent_functionElimination natural_numberEquality because_Cache sqequalRule lambdaEquality intEquality applyEquality functionExtensionality dependent_set_memberEquality productElimination independent_pairFormation unionElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality functionEquality equalityTransitivity equalitySymmetry applyLambdaEquality dependent_set_memberFormation

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: 2017_09_29-PM-05_57_59
Last ObjectModification: 2017_07_26-PM-02_04_07

Theory : list_1

Home Index