Nuprl Lemma : ma-ring_wf
R:Id List. s:{i:Id| (i 
R)} 
{i:Id| (i R)} . (ma-ring(R;s) 
)
Proof not projected
Definitions occuring in Statement :
ma-ring: ma-ring(R;s),
Id: Id,
prop: ,
all: x:A. B[x],
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
list: type List,
l_member: (x l)
Definitions :
universe: Type,
prop: ,
equal: s = t,
member: t T,
isect: 
x:A. B[x],
uall: [x:A]. B[x],
function: x:A B[x],
all: x:A. B[x],
l_member: (x l),
Id: Id,
set: {x:A| B[x]} ,
list: type List,
ma-ring: ma-ring(R;s),
and: P 
Q,
product: x:A 
B[x],
inject: Inj(A;B;f),
exists: 
x:A. B[x],
nat: 
,
limited-type: LimitedType,
apply: f a,
fun_exp: f^n
Lemmas :
fun_exp_wf,
Id_wf,
l_member_wf,
nat_wf,
inject_wf
\mforall{}R:Id List. \mforall{}s:\{i:Id| (i \mmember{} R)\} {}\mrightarrow{} \{i:Id| (i \mmember{} R)\} . (ma-ring(R;s) \mmember{} \mBbbP{})
Date html generated:
2012_02_20-PM-05_55_42
Last ObjectModification:
2012_02_02-PM-02_29_41
Home
Index