---

Step * of Lemma real-fun-implies-sfun-ext

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ].  real-sfun(f;a;b) supposing real-fun(f;a;b)
BY
{ Extract of Obid: real-fun-implies-sfun
  normalizes to:
  
  λx,y,_. eval m = 4 * rlessw(r0;|x - y|) in if ((x m) + 4) < (y m)  then inl m  else (inr m )
  
  not unfolding  rlessw int-to-real rsub rabs rmax rmin
  finishing with Reduce 0 }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[f:[a,  b]  {}\mrightarrow{}\mBbbR{}].    real-sfun(f;a;b)  supposing  real-fun(f;a;b)


By

---

Latex:
Extract  of  Obid:  real-fun-implies-sfun
normalizes  to:

\mlambda{}x,y,$_{}$.  eval  m  =  4  *  rlessw(r0;|x  -  y|)  in  if  ((x  m)  +  4)  <  (y  m)    then  inl  \000Cm    else  (inr  m  )

not  unfolding    rlessw  int-to-real  rsub  rabs  rmax  rmin
finishing  with  Reduce  0

---

Home Index