Nuprl Lemma : vr_RINV

Nuprl Lemma : vr_RINV_wf

[A,B:Type].

[f:A

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

')

Proof not projected

Definitions occuring in Statement : vr_RINV: vr_RINV(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_RINV: vr_RINV(f;A;B), exists:

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

B[x], all:

x:A. B[x], apply: f a

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