---

Step * of Lemma real-continuity1-ext

∀a,b:ℝ.
  ∀f:[a, b] ⟶ℝ
    ∀k:ℕ+. ∃d:{d:ℝ| r0 < d} . ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((|x - y| ≤ d) ⇒ (|(f x) - f y| ≤ (r1/r(k)))) 
    supposing ∀x,y:{x:ℝ| x ∈ [a, b]} .  ((x = y) ⇒ ((f x) = (f y))) 
  supposing a ≤ b
BY
{ Extract of Obid: real-continuity1
  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 tt  else (inr (λ_.⋅) )
                                              else if (4) < (-x)
                                                      then tt
                                                      else (inr (λ_.⋅) );x;λg.(f 
                                                                           cantor-to-interval(a;b;λi.if (i) < (x)
                                                                                                        then g i
                                                                                                        else ff) 
                                                                           (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.⋅, ⋅, ⋅>>
             else <r1, λx,y,%15,n. <λv.⋅, ⋅, ⋅>>
             fi  }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.
    \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}
        \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  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y))) 
    supposing  a  \mleq{}  b


By

---

Latex:
Extract  of  Obid:  real-continuity1
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  tt    else  (inr  (\mlambda{}$_{\mbackslash{}\000Cff7d$.\mcdot{})  )
                                                                                        else  if  (4)  <  (-x)
                                                                                                        then  tt
                                                                                                        else  (inr  (\mlambda{}$_{}$.\mcdot{})  );x;\mlambda{}g.\000C(f 
                                                                                                                                                cantor-to-interval(a;b;...) 
                                                                                                                                                (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,  \mlambda{}x,y,\%,n.  <\mlambda{}v.\mcdot{},  \mcdot{},  \mcdot{}>>
                      else  <r1,  \mlambda{}x,y,\%15,n.  <\mlambda{}v.\mcdot{},  \mcdot{},  \mcdot{}>>
                      fi 

---

Home Index