Nuprl Lemma : vr_SURJ

Nuprl Lemma : vr_SURJ_wf

[A,B:Type].

[f:A

B]. (vr_SURJ(f;A;B)

')

Proof not projected

Definitions occuring in Statement : vr_SURJ: vr_SURJ(f;A;B), uall:

[x:A]. B[x], member: t

T, function: x:A

B[x], universe: Type
Definitions : uall:

[x:A]. B[x], isect:

x:A. B[x], equal: s = t, member: t

T, universe: Type, axiom: Ax, function: x:A

B[x], vr_SURJ: vr_SURJ(f;A;B), all:

x:A. B[x], exists:

x:A. B[x], product: x:A

B[x], apply: f a

\mforall{}[A,B:Type]. \mforall{}[f:A {}\mrightarrow{} B]. (vr\_SURJ(f;A;B) \mmember{} \mBbbU{}') Date html generated: 2012_02_20-PM-03_34_34 Last ObjectModification: 2012_02_02-PM-01_55_35 Home Index