---

Step * of Lemma by-nearby-cases-ext

∀[P:ℝ ⟶ ℝ ⟶ ℙ]
  ∀n:ℕ+. ∀x:ℝ.
    ((∀y:{y:ℝ| x < y} . P[x;y])
    ⇒ (∀y:{y:ℝ| y < x} . P[x;y])
    ⇒ (∀y:{y:ℝ| |x - y| ≤ (r1/r(n))} . P[x;y])
    ⇒ (∀y:ℝ. P[x;y]))
BY
{ Extract of Obid: by-nearby-cases
  normalizes to:
  
  λn,x,A,B,C,y. eval m = 4 * n in
                eval a = x m in
                eval b = y m in
                  if (a + 4) < (b)  then A y  else if (b + 4) < (a)  then B y  else (C y)
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}  {}\mrightarrow{}  \mBbbP{}]
    \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}x:\mBbbR{}.
        ((\mforall{}y:\{y:\mBbbR{}|  x  <  y\}  .  P[x;y])
        {}\mRightarrow{}  (\mforall{}y:\{y:\mBbbR{}|  y  <  x\}  .  P[x;y])
        {}\mRightarrow{}  (\mforall{}y:\{y:\mBbbR{}|  |x  -  y|  \mleq{}  (r1/r(n))\}  .  P[x;y])
        {}\mRightarrow{}  (\mforall{}y:\mBbbR{}.  P[x;y]))


By

---

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

\mlambda{}n,x,A,B,C,y.  eval  m  =  4  *  n  in
                            eval  a  =  x  m  in
                            eval  b  =  y  m  in
                                if  (a  +  4)  <  (b)    then  A  y    else  if  (b  +  4)  <  (a)    then  B  y    else  (C  y)
finishing  with  Auto

---

Home Index