Nuprl Lemma : not_base_enumerable3
(
f:
Base. Surj(;Base;f))
Proof
Definitions occuring in Statement :
surject: Surj(A;B;f),
nat: ,
exists: x:A. B[x],
not: A,
function: x:A B[x],
base: Base
Definitions :
so_lambda: 
x.t[x],
member: t 
T,
implies: P 
Q,
not: A,
so_apply: x[s],
uall: 
[x:A]. B[x],
all: x:A. B[x],
false: False,
prop: 
Lemmas :
surject_wf,
nat_wf,
exists_wf,
not_base_decidble_eq_diag2,
base_wf,
surject_implies_decidble_eq2
\mneg{}(\mexists{}f:\mBbbN{} {}\mrightarrow{} Base. Surj(\mBbbN{};Base;f))
Date html generated:
2013_03_20-AM-09_48_24
Last ObjectModification:
2012_11_27-AM-10_32_01
Home
Index