Nuprl Lemma : RSC_incround

Nuprl Lemma : RSC_incround_wf

RSC_incround()

D,C,B,A:

'. (D

C

B

A

C)

Proof not projected

Definitions occuring in Statement : RSC_incround: RSC_incround(), member: t

T, isect:

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

B[x], product: x:A

B[x], universe: Type
Definitions : member: t

T, RSC_incround: RSC_incround()

RSC\_incround() \mmember{} \mcap{}D,C,B,A:\mBbbU{}'. (D \mtimes{} C \mtimes{} B {}\mrightarrow{} A {}\mrightarrow{} C) Date html generated: 2012_02_20-PM-03_59_23 Last ObjectModification: 2012_02_02-PM-01_58_33 Home Index