Nuprl Definition : max-f-class
(v from X with maximum f[v]) == accum-class(v1,v2.if f[v1] <z f[v2] then v2 else v1 fi ; v.v; X)
Definitions occuring in Statement :
accum-class: accum-class(a,x.f[a; x];x.base[x];X),
ifthenelse: if b then t else f fi ,
lt_int: i <z j
FDL editor aliases :
max-f-class
Latex:
(v from X with maximum f[v]) == accum-class(v1,v2.if f[v1] <z f[v2] then v2 else v1 fi ; v.v; X)
Date html generated:
2015_07_20-PM-03_49_12
Last ObjectModification:
2012_02_25-PM-01_55_53
Home
Index