### Nuprl Lemma : pigeon-hole-implies2

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

Proof

Definitions occuring in Statement :  inject: `Inj(A;B;f)` 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]` multiply: `n * m` 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: `ℕ` inject: `Inj(A;B;f)` implies: `P `` Q` prop: `ℙ` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` and: `P ∧ Q` int_seg: `{i..j-}` less_than: `a < b` less_than': `less_than'(a;b)` true: `True` squash: `↓T` lelt: `i ≤ j < k` guard: `{T}` sq_exists: `∃x:A [B[x]]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` bfalse: `ff` sq_type: `SQType(T)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  member-less_than equal_wf int_seg_wf pigeon-hole-implies-ext nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermMultiply_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf less_than_wf lelt_wf subtract_wf int_seg_properties itermSubtract_wf int_term_value_subtract_lemma decidable__lt lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf sq_stable__equal eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot inject_wf nat_wf decidable__equal_int intformeq_wf int_formula_prop_eq_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 multiplyEquality natural_numberEquality independent_isectElimination sqequalRule lambdaEquality dependent_functionElimination axiomEquality because_Cache applyEquality dependent_set_memberEquality unionElimination approximateComputation independent_functionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation lessCases baseClosed equalityTransitivity equalitySymmetry imageMemberEquality axiomSqEquality imageElimination productElimination functionExtensionality equalityElimination promote_hyp instantiate cumulativity functionEquality applyLambdaEquality dependent_set_memberFormation

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

Date html generated: 2019_06_20-PM-01_32_21
Last ObjectModification: 2018_08_20-PM-09_32_22

Theory : list_1

Home Index