Nuprl Definition : qpositive
qpositive(r) ==
let r' ⟵ r
in if isint(r') then 0 <z r' else let p,q = r' in (0 <z p ∧b 0 <z q) ∨b(p <z 0 ∧b q <z 0) fi
Definitions occuring in Statement :
bor: p ∨bq,
band: p ∧b q,
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
bfalse: ff,
btrue: tt,
isint: isint def,
spread: spread def,
natural_number: $n
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
isint: isint def,
btrue: tt,
bfalse: ff,
spread: spread def,
bor: p ∨bq,
band: p ∧b q,
lt_int: i <z j,
natural_number: $n
FDL editor aliases :
qpositive
Latex:
qpositive(r) ==
let r' \mleftarrow{}{} r
in if isint(r') then 0 <z r' else let p,q = r' in (0 <z p \mwedge{}\msubb{} 0 <z q) \mvee{}\msubb{}(p <z 0 \mwedge{}\msubb{} q <z 0) fi
Date html generated:
2016_05_15-PM-10_38_12
Last ObjectModification:
2015_09_23-AM-08_26_57
Theory : rationals
Home
Index