Nuprl Definition : is-half-interval

is-half-interval(I;J) ==  let a,b = I in let c,d = J in (qeq(a;c) ∧b qeq(b;qavg(c;d))) ∨b(qeq(a;qavg(c;d)) ∧b qeq(b;d))


Definitions occuring in Statement :  qavg: qavg(a;b),  qeq: qeq(r;s),  bor: p ∨bq,  band: p ∧b q,  spread: spread def
Definitions occuring in definition :  qeq: qeq(r;s),  qavg: qavg(a;b),  band: p ∧b q,  bor: p ∨bq,  spread: spread def
FDL editor aliases :  is-half-interval
Latex:
is-half-interval(I;J)  ==
    let  a,b  =  I 
    in  let  c,d  =  J 
          in  (qeq(a;c)  \mwedge{}\msubb{}  qeq(b;qavg(c;d)))  \mvee{}\msubb{}(qeq(a;qavg(c;d))  \mwedge{}\msubb{}  qeq(b;d))


Date html generated: 2019_10_29-AM-07_50_28
Last ObjectModification: 2019_10_21-PM-00_48_06

Theory : rationals


Home Index