### Nuprl Lemma : finite-injection

`∀[T:Type]`
`  ((∀x,y:T.  Dec(x = y ∈ T))`
`  `` (∀n:ℕ. ∀s:ℕn ⟶ T.  (Surj(ℕn;T;s) `` (∀f:T ⟶ T. ∀x:T. ∃m:ℕ+n + 1. ((f^m x) = x ∈ T) supposing Inj(T;T;f)))))`

Proof

Definitions occuring in Statement :  fun_exp: `f^n` surject: `Surj(A;B;f)` 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]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` add: `n + m` 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` inject: `Inj(A;B;f)` iff: `P `⇐⇒` Q` and: `P ∧ Q` exists: `∃x:A. B[x]` prop: `ℙ` nat: `ℕ` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` lelt: `i ≤ j < k` le: `A ≤ B` less_than: `a < b` squash: `↓T` ge: `i ≥ j ` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` so_apply: `x[s]` subtype_rel: `A ⊆r B` less_than': `less_than'(a;b)` guard: `{T}` true: `True` rev_implies: `P `` Q` cand: `A c∧ B` subtract: `n - m` sq_type: `SQType(T)`
Lemmas referenced :  surject-inverse inject_wf surject_wf int_seg_wf istype-nat decidable_wf equal_wf istype-universe decidable__exists_int_seg fun_exp_wf int_seg_properties nat_properties decidable__le full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf istype-le int_seg_subtype_nat istype-false set_subtype_base lelt_wf int_subtype_base squash_wf true_wf subtype_rel_self iff_weakening_equal decidable__lt subtract_wf itermSubtract_wf intformless_wf int_term_value_subtract_lemma int_formula_prop_less_lemma itermAdd_wf int_term_value_add_lemma istype-less_than fun_exp-injection fun_exp_add_apply minus-one-mul add-commutes add-associates add-mul-special zero-mul zero-add subtype_base_sq add-zero add-swap int_formula_prop_eq_lemma intformeq_wf decidable__equal_int pigeon-hole
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt cut introduction sqequalRule sqequalHypSubstitution lambdaEquality_alt dependent_functionElimination thin hypothesisEquality axiomEquality hypothesis functionIsTypeImplies inhabitedIsType rename extract_by_obid isectElimination because_Cache productElimination independent_functionElimination universeIsType functionIsType natural_numberEquality setElimination instantiate universeEquality addEquality applyEquality dependent_set_memberEquality_alt imageElimination unionElimination independent_isectElimination approximateComputation dependent_pairFormation_alt int_eqEquality Error :memTop,  independent_pairFormation voidElimination equalityIstype intEquality sqequalBase equalitySymmetry equalityTransitivity applyLambdaEquality imageMemberEquality baseClosed productIsType cumulativity

Latex:
\mforall{}[T:Type]
((\mforall{}x,y:T.    Dec(x  =  y))
{}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
(Surj(\mBbbN{}n;T;s)  {}\mRightarrow{}  (\mforall{}f:T  {}\mrightarrow{}  T.  \mforall{}x:T.  \mexists{}m:\mBbbN{}\msupplus{}n  +  1.  ((f\^{}m  x)  =  x)  supposing  Inj(T;T;f)))))

Date html generated: 2020_05_19-PM-09_43_47
Last ObjectModification: 2020_01_04-PM-08_18_24

Theory : list_1

Home Index