Nuprl Definition : ma-ring

ma-ring(R;s) == Inj({i:Id| (i

R)} ;{i:Id| (i

R)} ;s)

(

i,j:{i:Id| (i

R)} .

n:

. (j = (s^n i)))

Definitions occuring in Statement : Id: Id, inject: Inj(A;B;f), nat:

, all:

x:A. B[x], exists:

x:A. B[x], and: P

Q, set: {x:A| B[x]} , apply: f a, equal: s = t, l_member: (x

l), fun_exp: f^n
FDL editor aliases : ma-ring

ma-ring(R;s) == Inj(\{i:Id| (i \mmember{} R)\} ;\{i:Id| (i \mmember{} R)\} ;s) \mwedge{} (\mforall{}i,j:\{i:Id| (i \mmember{} R)\} . \mexists{}n:\mBbbN{}. (j = (s\^{}n\000C i))) Date html generated: 2012_02_20-PM-05_55_36 Last ObjectModification: 2012_02_02-PM-02_29_38 Home Index