Nuprl Definition : rless-witness

rless-witness(x;y;p) ==  fst((TERMOF{rless-implies-rleq:o, 1:l} x y p))


Definitions occuring in Statement :  pi1: fst(t),  apply: f a
Definitions occuring in definition :  pi1: fst(t),  apply: f a
TermOfs occuring in Definition :  rless-implies-rleq
FDL editor aliases :  rless-witness rless-witness
Latex:
rless-witness(x;y;p)  ==    fst((TERMOF\{rless-implies-rleq:o,  1:l\}  x  y  p))


Date html generated: 2016_05_18-AM-07_53_53
Last ObjectModification: 2015_09_23-AM-09_02_58

Theory : reals


Home Index