Nuprl Lemma : aa_not_total_enumerable
(f:    . Surj(;  f))
Proof
Definitions occuring in Statement : 
surject: Surj(A;B;f), 
bool: , 
nat: , 
exists: x:A. B[x], 
not: A, 
function: x:A  B[x]
Definitions : 
not: A, 
implies: P  Q, 
member: t  T, 
so_lambda: x.t[x], 
all: x:A. B[x], 
exists: x:A. B[x], 
iff: P  Q, 
and: P  Q, 
rev_implies: P  Q, 
bnot: b, 
btrue: tt, 
ifthenelse: if b then t else f fi , 
assert: b, 
bfalse: ff, 
true: True, 
surject: Surj(A;B;f), 
uall: [x:A]. B[x], 
so_apply: x[s], 
bool: , 
false: False, 
unit: Unit, 
uimplies: b supposing a, 
uiff: uiff(P;Q), 
prop: , 
sq_type: SQType(T), 
guard: {T}, 
it:
Lemmas : 
exists_wf, 
nat_wf, 
bool_wf, 
surject_wf, 
bnot_wf, 
assert_wf, 
all_wf, 
iff_wf, 
eqtt_to_assert, 
uiff_transitivity, 
equal_wf, 
not_wf, 
eqff_to_assert, 
assert_of_bnot, 
btrue_neq_bfalse, 
assert_elim, 
bfalse_wf, 
and_wf, 
subtype_base_sq, 
bool_subtype_base, 
not_assert_elim, 
btrue_wf
\mneg{}(\mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  Surj(\mBbbN{};\mBbbN{}  {}\mrightarrow{}  \mBbbB{};f))
Date html generated:
2013_03_20-AM-09_49_28
Last ObjectModification:
2012_11_27-AM-10_32_04
Home
Index