### Nuprl Lemma : not-inject

`∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) `` (∀n:ℕ. ∀f:ℕn ⟶ T.  ∃i:ℕn. ∃j:ℕi. ((f i) = (f j) ∈ T) supposing ¬Inj(ℕn;T;f)))`

Proof

Definitions occuring in Statement :  inject: `Inj(A;B;f)` int_seg: `{i..j-}` nat: `ℕ` decidable: `Dec(P)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` not: `¬A` false: `False` nat: `ℕ` prop: `ℙ` inject: `Inj(A;B;f)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` iff: `P `⇐⇒` Q` and: `P ∧ Q` exists: `∃x:A. B[x]` int_seg: `{i..j-}` decidable: `Dec(P)` or: `P ∨ Q` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` guard: `{T}` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top`
Lemmas referenced :  int_term_value_constant_lemma int_formula_prop_le_lemma itermConstant_wf intformle_wf decidable__le int_formula_prop_eq_lemma intformeq_wf decidable__equal_int exists_wf int_formula_prop_wf int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt nat_properties int_seg_properties lelt_wf decidable__lt decidable_wf nat_wf not_wf decidable__equal_int_seg decidable__implies decidable__all_int_seg equal_wf all_wf not-all-int_seg int_seg_wf inject_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction sqequalRule sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality voidElimination lemma_by_obid isectElimination natural_numberEquality setElimination rename hypothesis functionEquality applyEquality independent_functionElimination instantiate because_Cache isect_memberEquality productElimination universeEquality unionElimination dependent_pairFormation dependent_set_memberEquality independent_pairFormation equalitySymmetry cumulativity independent_isectElimination int_eqEquality intEquality voidEquality computeAll

Latex:
\mforall{}[T:Type]
((\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}f:\mBbbN{}n  {}\mrightarrow{}  T.    \mexists{}i:\mBbbN{}n.  \mexists{}j:\mBbbN{}i.  ((f  i)  =  (f  j))  supposing  \mneg{}Inj(\mBbbN{}n;T;f)))

Date html generated: 2016_05_14-AM-07_27_06
Last ObjectModification: 2016_01_14-PM-09_59_50

Theory : int_2

Home Index