Nuprl Definition : imax-class
(maximum f[v] ≥ lb with v from X) == es-interface-accum(λmx,v. imax(mx;f[v]);lb;X)
Definitions occuring in Statement :
es-interface-accum: es-interface-accum(f;x;X),
imax: imax(a;b),
lambda: λx.A[x]
FDL editor aliases :
imax-class
Latex:
(maximum f[v] \mgeq{} lb with v from X) == es-interface-accum(\mlambda{}mx,v. imax(mx;f[v]);lb;X)
Date html generated:
2015_07_20-PM-03_46_50
Last ObjectModification:
2012_02_25-PM-01_54_52
Home
Index