---

Step * of Lemma real-weak-Markov-ext

∀x,y:ℝ.  x ≠ y supposing ∀z:ℝ. ((¬(z = x)) ∨ (¬(z = y)))
BY
{ Extract of Obid: real-weak-Markov
  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  int-to-real rsub rminus rabs rlessw
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    x  \mneq{}  y  supposing  \mforall{}z:\mBbbR{}.  ((\mneg{}(z  =  x))  \mvee{}  (\mneg{}(z  =  y)))


By

---

Latex:
Extract  of  Obid:  real-weak-Markov
normalizes  to:

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

not  unfolding    int-to-real  rsub  rminus  rabs  rlessw
finishing  with  Auto

---

Home Index