Nuprl Definition : bigrel
If for R a relation on T (i.e. a member of type T ⟶ T ⟶ ℙ)
F(R) is another relation on T, then νR.F[R] is meant to be the
greatest relation on T that is a fixed point of F.
If F has the properties 
rel-monotone{i:l}(T;R.F[R]) and 
rel-continuous{i:l}(T;R.F[R])
then this will be so 
(see bigrel-iff) ⋅
νR.F[R] ==  ⋂n:ℕ. primrec(n;λx,y. True;λm,R. F[R])
Definitions occuring in Statement : 
isect-rel: ⋂i:T. R[i]
, 
primrec: primrec(n;b;c)
, 
nat: ℕ
, 
true: True
, 
lambda: λx.A[x]
Definitions occuring in definition : 
isect-rel: ⋂i:T. R[i]
, 
nat: ℕ
, 
primrec: primrec(n;b;c)
, 
true: True
, 
lambda: λx.A[x]
FDL editor aliases : 
bigrel
Latex:
\mnu{}R.F[R]  ==    \mcap{}n:\mBbbN{}.  primrec(n;\mlambda{}x,y.  True;\mlambda{}m,R.  F[R])
Date html generated:
2019_06_20-PM-00_31_29
Last ObjectModification:
2018_11_29-PM-01_53_09
Theory : relations
Home
Index