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: P ⇒ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ 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