---

Step * of Lemma real-continuity2-ext

∀a,b:ℝ.
  ∀f:[a, b] ⟶ℝ
    ((∀x,y:{x:ℝ| x ∈ [a, b]} .  (f x ≠ f y ⇒ x ≠ y))
    ⇒ (∀k:ℕ+. ∃d:{d:ℝ| r0 < d} . ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((|x - y| ≤ d) ⇒ (|(f x) - f y| ≤ (r1/r(k)))))) 
  supposing a ≤ b
BY
{ Extract of Obid: real-continuity2
  not unfolding  recops exp realops realcont real-cont-br real-cont-ps
  finishing with Auto
  normalizes to:
  
  λa,b,f,_,k.
             eval x = real-cont-br(a; b; f; k; 4) - 1 in
             eval x = real-cont-ps(k;a;b;f;x;4) in
               if finite-cantor-decider(λx,y.
                                             eval x = x - y in
                                             if (0) < (x)
                                                then if (4) < (x)  then inl Ax  else (inr (λ_.Ax) )
                                                else if (4) < (-x)
                                                        then inl Ax
                                                        else (inr (λ_.Ax) );x;λg.(f 
                                                                              cantor-to-interval(a;b;λi.if (i) < (x)
                                                                                                           then g i
                                                                                                           else ...) 
                                                                              (4 * k)))
               then eval x = real-cont-br(a; b; f; k; 2) - 1 in
                    eval m = real-cont-ps(k;a;b;f;x;2) in
                      <(2^m * b - a)/6 * 3^m, λx,y,_,n. <λv.Ax, Ax, Ax>>
               else <r1, λx,y,_,n. <λv.Ax, Ax, Ax>>
               fi  }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}
        ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    (f  x  \mneq{}  f  y  {}\mRightarrow{}  x  \mneq{}  y))
        {}\mRightarrow{}  (\mforall{}k:\mBbbN{}\msupplus{}
                    \mexists{}d:\{d:\mBbbR{}|  r0  <  d\} 
                      \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((|x  -  y|  \mleq{}  d)  {}\mRightarrow{}  (|(f  x)  -  f  y|  \mleq{}  (r1/r(k)))))) 
    supposing  a  \mleq{}  b


By

---

Latex:
Extract  of  Obid:  real-continuity2
not  unfolding    recops  exp  realops  realcont  real-cont-br  real-cont-ps
finishing  with  Auto
normalizes  to:

\mlambda{}a,b,f,$_{}$,k.
                    eval  x  =  real-cont-br(a;  b;  f;  k;  4)  -  1  in
                    eval  x  =  real-cont-ps(k;a;b;f;x;4)  in
                        if  finite-cantor-decider(\mlambda{}x,y.
                                                                                    eval  x  =  x  -  y  in
                                                                                    if  (0)  <  (x)
                                                                                          then  if  (4)  <  (x)    then  inl  Ax    else  (inr  (\mlambda{}$_\mbackslash{}\000Cff7b}$.Ax)  )
                                                                                          else  if  (4)  <  (-x)    then  inl  Ax    else  (inr  (\mlambda{}$_\000C{}$.Ax)  );x;...)
                        then  eval  x  =  real-cont-br(a;  b;  f;  k;  2)  -  1  in
                                  eval  m  =  real-cont-ps(k;a;b;f;x;2)  in
                                      <(2\^{}m  *  b  -  a)/6  *  3\^{}m,  \mlambda{}x,y,$_{}$,n.  <\mlambda{}v.Ax,  Ax,  Ax>>
                        else  <r1,  \mlambda{}x,y,$_{}$,n.  <\mlambda{}v.Ax,  Ax,  Ax>>
                        fi 

---

Home Index