Nuprl Lemma : decidable__equal_injection
∀n:ℕ. ∀T:Type. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀f,g:ℕn →⟶ T. Dec(f = g ∈ ℕn →⟶ T)))
Proof
Definitions occuring in Statement :
injection: A →⟶ B,
int_seg: {i..j-},
nat: ℕ,
decidable: Dec(P),
all: ∀x:A. B[x],
implies: P ⇒ Q,
natural_number: $n,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
so_apply: x[s],
prop: ℙ,
so_lambda: λ2x.t[x],
nat: ℕ,
member: t ∈ T,
uall: ∀[x:A]. B[x],
injection: A →⟶ B,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
nat_wf,
equal_wf,
decidable_wf,
all_wf,
injection_wf,
inject_wf,
compact-finite,
decidable__equal_compact_domain,
int_seg_wf,
decidable__equal_set
Rules used in proof :
universeEquality,
applyEquality,
functionExtensionality,
lambdaEquality,
sqequalRule,
dependent_functionElimination,
because_Cache,
independent_functionElimination,
cumulativity,
hypothesis,
hypothesisEquality,
rename,
setElimination,
natural_numberEquality,
functionEquality,
thin,
isectElimination,
extract_by_obid,
introduction,
cut,
sqequalHypSubstitution,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}n:\mBbbN{}. \mforall{}T:Type. ((\mforall{}x,y:T. Dec(x = y)) {}\mRightarrow{} (\mforall{}f,g:\mBbbN{}n \mrightarrow{}{}\mrightarrow{} T. Dec(f = g)))
Date html generated:
2018_05_21-PM-08_17_07
Last ObjectModification:
2017_12_15-PM-00_02_00
Theory : general
Home
Index