Nuprl Definition : down-closed
down-closed(T;X) == R-closed(T List;s.X s;bs,as.as ≤ bs)
Definitions occuring in Statement :
R-closed: R-closed(T;x.X[x];a,b.R[a; b]),
iseg: l1 ≤ l2,
list: T List,
apply: f a
Definitions occuring in definition :
R-closed: R-closed(T;x.X[x];a,b.R[a; b]),
list: T List,
apply: f a,
iseg: l1 ≤ l2
FDL editor aliases :
down-closed
Latex:
down-closed(T;X) == R-closed(T List;s.X s;bs,as.as \mleq{} bs)
Date html generated:
2016_05_14-PM-04_09_57
Last ObjectModification:
2015_09_22-PM-06_02_18
Theory : fan-theorem
Home
Index