### Nuprl Lemma : fun_exp-injection

`∀[T:Type]. ∀[f:T ⟶ T].  ∀[n:ℕ]. Inj(T;T;f^n) supposing Inj(T;T;f)`

Proof

Definitions occuring in Statement :  fun_exp: `f^n` inject: `Inj(A;B;f)` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` guard: `{T}` prop: `ℙ` inject: `Inj(A;B;f)` all: `∀x:A. B[x]` top: `Top` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` sq_type: `SQType(T)` compose: `f o g`
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf equal_wf fun_exp_wf fun_exp0_lemma le_wf decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel le_weakening2 nat_wf inject_wf subtype_base_sq int_subtype_base not-le-2 fun_exp1_lemma fun_exp_add-sq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination independent_functionElimination voidElimination sqequalRule lambdaEquality dependent_functionElimination axiomEquality cumulativity applyEquality because_Cache functionExtensionality isect_memberEquality voidEquality dependent_set_memberEquality unionElimination independent_pairFormation productElimination addEquality intEquality minusEquality equalityTransitivity equalitySymmetry functionEquality universeEquality instantiate

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  T].    \mforall{}[n:\mBbbN{}].  Inj(T;T;f\^{}n)  supposing  Inj(T;T;f)

Date html generated: 2017_04_14-AM-07_34_56
Last ObjectModification: 2017_02_27-PM-03_07_53

Theory : fun_1

Home Index