---

Step * of Lemma near-inverse-of-increasing-function-ext

∀f:ℝ ⟶ ℝ. ∀n,M:ℕ+. ∀z:ℝ. ∀a,b:ℤ.
  ∀k:ℕ+
    (∃c:ℤ. (∃j:ℕ+ [((|f[(r(c))/j] - z| ≤ (r1/r(n))) ∧ ((r(a))/k ≤ (r(c))/j) ∧ ((r(c))/j ≤ (r(b))/k))])) supposing 
       ((z ≤ f[(r(b))/k]) and 
       (f[(r(a))/k] ≤ z) and 
       (∀x,y:ℝ.
          (((r(a))/k ≤ x)
          ⇒ (x < y)
          ⇒ (y ≤ (r(b))/k)
          ⇒ ((f[x] ≤ f[y]) ∧ (((y - x) ≤ (r1/r(M))) ⇒ ((f[y] - f[x]) ≤ (r1/r(n)))))))) 
  supposing a < b
BY
{ Extract of Obid: near-inverse-of-increasing-function
  not unfolding  primrec recdefs int-rdiv int-to-real
  finishing with Auto
  normalizes to:
  
  λf,n,M,z,a,b,k. if ((M * (b - a)) - k) < (0)
                     then <b, k>
                     else (letrec g(a)=λb,k. if (k) < (M * (b - a))
                                                then eval m = a + b in
                                                     eval j = 2 * k in
                                                     eval n4 = 4 * n in
                                                     eval a1 = f (r(m))/j n4 in
                                                     eval b1 = z n4 in
                                                       if (a1 + 4) < (b1)
                                                          then eval bb = 2 * b in
                                                               let c,N = g m bb j 
                                                               in <c, N>
                                                          else if (b1 + 4) < (a1)
                                                                  then eval aa = 2 * a in
                                                                       let c,N = g aa m j 
                                                                       in <c, N>
                                                                  else <m, j>
                                                else <b, k> in
                            g(a) 
                           b 
                           k) }

---

Latex:

---

Latex:
\mforall{}f:\mBbbR{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}n,M:\mBbbN{}\msupplus{}.  \mforall{}z:\mBbbR{}.  \mforall{}a,b:\mBbbZ{}.
    \mforall{}k:\mBbbN{}\msupplus{}
        (\mexists{}c:\mBbbZ{}
            (\mexists{}j:\mBbbN{}\msupplus{}  [((|f[(r(c))/j]  -  z|  \mleq{}  (r1/r(n)))
                          \mwedge{}  ((r(a))/k  \mleq{}  (r(c))/j)
                          \mwedge{}  ((r(c))/j  \mleq{}  (r(b))/k))]))  supposing 
              ((z  \mleq{}  f[(r(b))/k])  and 
              (f[(r(a))/k]  \mleq{}  z)  and 
              (\mforall{}x,y:\mBbbR{}.
                    (((r(a))/k  \mleq{}  x)
                    {}\mRightarrow{}  (x  <  y)
                    {}\mRightarrow{}  (y  \mleq{}  (r(b))/k)
                    {}\mRightarrow{}  ((f[x]  \mleq{}  f[y])  \mwedge{}  (((y  -  x)  \mleq{}  (r1/r(M)))  {}\mRightarrow{}  ((f[y]  -  f[x])  \mleq{}  (r1/r(n)))))))) 
    supposing  a  <  b


By

---

Latex:
Extract  of  Obid:  near-inverse-of-increasing-function
not  unfolding    primrec  recdefs  int-rdiv  int-to-real
finishing  with  Auto
normalizes  to:

\mlambda{}f,n,M,z,a,b,k.  if  ((M  *  (b  -  a))  -  k)  <  (0)
                                      then  <b,  k>
                                      else  (letrec  g(a)=\mlambda{}b,k.  if  (k)  <  (M  *  (b  -  a))
                                                                                            then  eval  m  =  a  +  b  in
                                                                                                      eval  j  =  2  *  k  in
                                                                                                      eval  n4  =  4  *  n  in
                                                                                                      eval  a1  =  f  (r(m))/j  n4  in
                                                                                                      eval  b1  =  z  n4  in
                                                                                                          if  (a1  +  4)  <  (b1)
                                                                                                                then  eval  bb  =  2  *  b  in
                                                                                                                          let  c,N  =  g  m  bb  j 
                                                                                                                          in  <c,  N>
                                                                                                                else  if  (b1  +  4)  <  (a1)
                                                                                                                                then  eval  aa  =  2  *  a  in
                                                                                                                                          let  c,N  =  g  aa  m  j 
                                                                                                                                          in  <c,  N>
                                                                                                                                else  <m,  j>
                                                                                            else  <b,  k>  in
                                                    g(a) 
                                                  b 
                                                  k)

---

Home Index