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