Nuprl Lemma : injection-inverse2
∀n:ℕ. ∀f:ℕn →⟶ ℕn. ∃g:ℕn →⟶ ℕn. ((∀a:ℕn. ((g (f a)) = a ∈ ℕn)) ∧ (∀a:ℕn. ((f (g a)) = a ∈ ℕn)))
Proof
Definitions occuring in Statement :
injection: A →⟶ B,
int_seg: {i..j-},
nat: ℕ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
natural_number: $n,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
nat: ℕ,
injection: A →⟶ B,
implies: P ⇒ Q,
exists: ∃x:A. B[x],
and: P ∧ Q,
cand: A c∧ B,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
inject: Inj(A;B;f),
squash: ↓T,
true: True,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
iff: P ⇐⇒ Q
Lemmas referenced :
injection-bijection,
injection_wf,
int_seg_wf,
nat_wf,
biject-inverse,
all_wf,
equal_wf,
inject_wf,
squash_wf,
true_wf,
iff_weakening_equal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
natural_numberEquality,
setElimination,
rename,
hypothesis,
because_Cache,
independent_functionElimination,
productElimination,
dependent_pairFormation,
independent_pairFormation,
productEquality,
sqequalRule,
lambdaEquality,
applyEquality,
dependent_set_memberEquality,
functionExtensionality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
universeEquality,
equalityUniverse,
levelHypothesis,
imageMemberEquality,
baseClosed,
independent_isectElimination
Latex:
\mforall{}n:\mBbbN{}. \mforall{}f:\mBbbN{}n \mrightarrow{}{}\mrightarrow{} \mBbbN{}n. \mexists{}g:\mBbbN{}n \mrightarrow{}{}\mrightarrow{} \mBbbN{}n. ((\mforall{}a:\mBbbN{}n. ((g (f a)) = a)) \mwedge{} (\mforall{}a:\mBbbN{}n. ((f (g a)) = a)))
Date html generated:
2018_05_21-PM-08_16_20
Last ObjectModification:
2017_07_26-PM-05_50_32
Theory : general
Home
Index