Nuprl Lemma : enumerable_implies_decidble_eq
T:Type. ((
f:
T. Bij(;T;f)) 
(t1,t2:T. Dec(t1 = t2)))
Proof
Definitions occuring in Statement :
biject: Bij(A;B;f),
nat: ,
decidable: Dec(P),
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
function: x:A B[x],
universe: Type,
equal: s = t
Definitions :
so_lambda: 
x.t[x],
member: t 
T,
implies: P Q,
all: x:A. B[x],
false: False,
not: 
A,
decidable: Dec(P),
and: P 
Q,
or: P 
Q,
true: True,
squash: 
T,
prop: 
,
guard: {T},
so_apply: x[s],
uall: [x:A]. B[x],
surject: Surj(A;B;f),
inject: Inj(A;B;f),
biject: Bij(A;B;f),
exists: x:A. B[x],
nat:
Lemmas :
biject_wf,
nat_wf,
exists_wf,
not_wf,
equal_wf,
and_wf,
true_wf,
squash_wf
\mforall{}T:Type. ((\mexists{}f:\mBbbN{} {}\mrightarrow{} T. Bij(\mBbbN{};T;f)) {}\mRightarrow{} (\mforall{}t1,t2:T. Dec(t1 = t2)))
Date html generated:
2013_03_20-AM-09_47_47
Last ObjectModification:
2012_11_27-AM-10_32_00
Home
Index