Nuprl Lemma : injection-inverse

[A,B:Type].  ∀f:A →⟶ B. (A  finite-type(A)  (∀x,y:B.  Dec(x y ∈ B))  (∃g:B ⟶ A. ∀a:A. ((g (f a)) a ∈ A)))


Proof




Definitions occuring in Statement :  injection: A →⟶ B finite-type: finite-type(T) decidable: Dec(P) uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] all: x:A. B[x] implies:  Q finite-type: finite-type(T) exists: x:A. B[x] member: t ∈ T prop: so_lambda: λ2x.t[x] so_apply: x[s] nat: injection: A →⟶ B decidable: Dec(P) or: P ∨ Q pi1: fst(t) guard: {T} inject: Inj(A;B;f) not: ¬A false: False surject: Surj(A;B;f)
Lemmas referenced :  all_wf decidable_wf equal_wf finite-type_wf injection_wf decidable__exists_int_seg int_seg_wf exists_wf not_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation rename sqequalHypSubstitution productElimination thin cut lemma_by_obid isectElimination hypothesisEquality sqequalRule lambdaEquality hypothesis universeEquality instantiate dependent_functionElimination natural_numberEquality setElimination applyEquality independent_functionElimination dependent_pairFormation unionEquality unionElimination equalityTransitivity equalitySymmetry cumulativity because_Cache voidElimination

Latex:
\mforall{}[A,B:Type].
    \mforall{}f:A  \mrightarrow{}{}\mrightarrow{}  B.  (A  {}\mRightarrow{}  finite-type(A)  {}\mRightarrow{}  (\mforall{}x,y:B.    Dec(x  =  y))  {}\mRightarrow{}  (\mexists{}g:B  {}\mrightarrow{}  A.  \mforall{}a:A.  ((g  (f  a))  =  a)))



Date html generated: 2016_05_15-PM-06_11_25
Last ObjectModification: 2015_12_27-PM-00_14_11

Theory : general


Home Index