Def  complete_intseg_mset(a; b; f)(x) == if a  x < b f(x) else 0 fi

is mentioned by

Thm*  a,b:, f:({a..b}), x:{a..b}. complete_intseg_mset(a; b; f)(x) = f(x)	[complete_intseg_mset_isext]
Thm*  a,b:, f:({a..b}), x:. Thm*  a  x < b  complete_intseg_mset(a; b; f)(x) = 0	[complete_intseg_mset_ismin]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html