Nuprl Definition : prec
prec(lbl,p.a[lbl; p];i) == {x:pcorec(lbl,p.a[lbl; p]) i| (pcorec-size(lbl,p.a[lbl; p]) i x)↓}
Definitions occuring in Statement :
pcorec-size: pcorec-size(lbl,p.a[lbl; p]),
pcorec: pcorec(lbl,p.a[lbl; p]),
has-value: (a)↓,
set: {x:A| B[x]} ,
apply: f a
Definitions occuring in definition :
set: {x:A| B[x]} ,
pcorec: pcorec(lbl,p.a[lbl; p]),
has-value: (a)↓,
apply: f a,
pcorec-size: pcorec-size(lbl,p.a[lbl; p])
FDL editor aliases :
p-rec
Latex:
prec(lbl,p.a[lbl; p];i) == \{x:pcorec(lbl,p.a[lbl; p]) i| (pcorec-size(lbl,p.a[lbl; p]) i x)\mdownarrow{}\}
Date html generated:
2019_06_20-PM-02_04_20
Last ObjectModification:
2019_02_21-PM-03_59_38
Theory : tuples
Home
Index