Nuprl Definition : q_le
q_le(r;s) == let r' ⟵ r in let s' ⟵ s in qpositive(s' - r') ∨bqeq(r';s')
Definitions occuring in Statement :
qsub: r - s,
qpositive: qpositive(r),
qeq: qeq(r;s),
bor: p ∨bq,
callbyvalueall: callbyvalueall
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
bor: p ∨bq,
qpositive: qpositive(r),
qsub: r - s,
qeq: qeq(r;s)
FDL editor aliases :
q_le
Latex:
q\_le(r;s) == let r' \mleftarrow{}{} r in let s' \mleftarrow{}{} s in qpositive(s' - r') \mvee{}\msubb{}qeq(r';s')
Date html generated:
2016_05_15-PM-10_40_35
Last ObjectModification:
2015_09_23-AM-08_27_03
Theory : rationals
Home
Index