Nuprl Lemma : not_total_enumerable

(

f:

. Surj(

;

;f))

Proof

Definitions occuring in Statement : surject: Surj(A;B;f), bool:

, exists:

x:A. B[x], not:

A, function: x:A

B[x], int:

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], prop:

, sq_type: SQType(T), uimplies: b supposing a, guard: {T}, bool:

, false: False, unit: Unit, uiff: uiff(P;Q), it:

Lemmas : exists_wf, bool_wf, surject_wf, bnot_wf, assert_wf, all_wf, iff_wf, and_wf, equal_wf, subtype_base_sq, int_subtype_base, eqtt_to_assert, uiff_transitivity, not_wf, eqff_to_assert, assert_of_bnot, btrue_neq_bfalse, assert_elim, bfalse_wf, bool_subtype_base, not_assert_elim, btrue_wf
\mneg{}(\mexists{}f:\mBbbZ{} {}\mrightarrow{} \mBbbZ{} {}\mrightarrow{} \mBbbB{}. Surj(\mBbbZ{};\mBbbZ{} {}\mrightarrow{} \mBbbB{};f)) Date html generated: 2013_03_20-AM-09_49_37 Last ObjectModification: 2012_11_27-AM-10_32_04 Home Index