---

Step * of Lemma nearby-cases-ext

∀n:ℕ+. ∀x,y:ℝ.  ((x < y) ∨ (y < x) ∨ (|x - y| ≤ (r1/r(n))))
BY
{ Extract of Obid: nearby-cases
  normalizes to:
  
  λn,x,y. eval m = 4 * n in
          eval a = x m in
          eval b = y m in
            if (a + 4) < (b)
               then inl m
               else if (b + 4) < (a)  then inr (inl m)   else (inr inr (λn.<λv.Ax, Ax, Ax>)  )
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x,y:\mBbbR{}.    ((x  <  y)  \mvee{}  (y  <  x)  \mvee{}  (|x  -  y|  \mleq{}  (r1/r(n))))


By

---

Latex:
Extract  of  Obid:  nearby-cases
normalizes  to:

\mlambda{}n,x,y.  eval  m  =  4  *  n  in
                eval  a  =  x  m  in
                eval  b  =  y  m  in
                    if  (a  +  4)  <  (b)
                          then  inl  m
                          else  if  (b  +  4)  <  (a)    then  inr  (inl  m)      else  (inr  inr  (\mlambda{}n.<\mlambda{}v.Ax,  Ax,  Ax>)    )
finishing  with  Auto

---

Home Index