---

Step * of Lemma real-continuity-ext

∀a,b:ℝ.  ∀f:[a, b] ⟶ℝ. real-cont(f;a;b) supposing real-fun(f;a;b) supposing a ≤ b
BY
{ Extract of Obid: real-continuity
  not unfolding  recops exp realops realcont
  finishing with (Try (Folds ``bottom it`` 0)
                  THEN Try (Folds ``btrue bfalse`` 0)
                  THEN Try (Folds ``real-cont-ps real-cont-br`` 0)
                  THEN 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{}.  real-cont(f;a;b)  supposing  real-fun(f;a;b)  supposing  a  \mleq{}  b


By

---

Latex:
Extract  of  Obid:  real-continuity
not  unfolding    recops  exp  realops  realcont
finishing  with  (Try  (Folds  ``bottom  it``  0)
                                THEN  Try  (Folds  ``btrue  bfalse``  0)
                                THEN  Try  (Folds  ``real-cont-ps  real-cont-br``  0)
                                THEN  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