---

Step * of Lemma rless-iff2-ext

∀x,y:ℝ.  (x < y ⇐⇒ ∃n:ℕ+. (x n) + 4 < y n)
BY
{ Extract of Obid: rless-iff2
  not unfolding  radd int-to-real rmul rminus rdiv mu
  finishing with Auto
  normalizes to:
  
  λx,y. <λn.<n, Ax>, λp.(fst(p))> }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (x  <  y  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}\msupplus{}.  (x  n)  +  4  <  y  n)


By

---

Latex:
Extract  of  Obid:  rless-iff2
not  unfolding    radd  int-to-real  rmul  rminus  rdiv  mu
finishing  with  Auto
normalizes  to:

\mlambda{}x,y.  <\mlambda{}n.<n,  Ax>,  \mlambda{}p.(fst(p))>

---

Home Index