Nuprl Lemma : rsc2_thr_out_wf
rsc2_thr_out() 
B,A:
'. (Id 
B A bag(B))
Proof not projected
Definitions occuring in Statement :
rsc2_thr_out: rsc2_thr_out(),
Id: Id,
member: t T,
isect: x:A. B[x],
function: x:A B[x],
universe: Type,
bag: bag(T)
Definitions :
rsc2_thr_out: rsc2_thr_out(),
member: t T,
all: 
x:A. B[x]
Lemmas :
Id_wf,
single-bag_wf
rsc2\_thr\_out() \mmember{} \mcap{}B,A:\mBbbU{}'. (Id {}\mrightarrow{} B {}\mrightarrow{} A {}\mrightarrow{} bag(B))
Date html generated:
2012_02_20-PM-04_42_01
Last ObjectModification:
2012_02_02-PM-02_05_36
Home
Index