Nuprl Lemma : rational_set

Nuprl Lemma : rational_set_blt

∀[r,s:ℚ].
(r <_b s ~ if isint(r)

  then if isint(s) then r <z s else let i,j = s in if 0 <z j then j * r <z i else i <z j * r fi  fi

  else let p,q = r
       in if isint(s)
          then if 0 <z q then p <z q * s else q * s <z p fi
          else let i,j = s
               in if 0 <z q * j then j * p <z q * i else q * i <z j * p fi
          fi
  fi )

Proof

Error : references

Latex:
\mforall{}[r,s:\mBbbQ{}]. (r <\msubb{} s \msim{} if isint(r) then if isint(s) then r <z s else let i,j = s in if 0 <z j then j * r <z i else i <z j * r fi fi else let p,q = r in if isint(s) then if 0 <z q then p <z q * s else q * s <z p fi else let i,j = s in if 0 <z q * j then j * p <z q * i else q * i <z j * p fi fi fi ) Date html generated: 2020_05_20-AM-09_15_59 Last ObjectModification: 2020_02_05-PM-02_34_48 Theory : rationals Home Index