---

Step * of Lemma common-limit-squeeze-ext

∀a,b,c:ℕ ⟶ ℝ.
  ((∀n:ℕ. ((a[n] ≤ a[n + 1]) ∧ (a[n + 1] ≤ b[n + 1]) ∧ (b[n + 1] ≤ b[n])))
  ⇒ lim n→∞.c[n] = r0
  ⇒ (∀n:ℕ. r0≤b[n] - a[n]≤c[n])
  ⇒ (∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)))
BY
{ Extract of Obid: common-limit-squeeze
  not unfolding  divide
  finishing with Auto
  normalizes to:
  
  λa,b,c,_,inf,_. <λn.eval m = 4 * n in
                      (a (inf m) m) ÷ 4
                  , λk.((inf (4 * k)) + 1)
                  , λk.eval a@0 = inf (2 * k) in
                       eval b = (inf (4 * 2 * k)) + 1 in
                         if (b) < (a@0)  then a@0  else b> }

---

Latex:

---

Latex:
\mforall{}a,b,c:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}n:\mBbbN{}.  ((a[n]  \mleq{}  a[n  +  1])  \mwedge{}  (a[n  +  1]  \mleq{}  b[n  +  1])  \mwedge{}  (b[n  +  1]  \mleq{}  b[n])))
    {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.c[n]  =  r0
    {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  r0\mleq{}b[n]  -  a[n]\mleq{}c[n])
    {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  (lim  n\mrightarrow{}\minfty{}.a[n]  =  y  \mwedge{}  lim  n\mrightarrow{}\minfty{}.b[n]  =  y)))


By

---

Latex:
Extract  of  Obid:  common-limit-squeeze
not  unfolding    divide
finishing  with  Auto
normalizes  to:

\mlambda{}a,b,c,$_{}$,inf,$_{}$.  <\mlambda{}n.eval  m  =  4  *  n  in
                                    (a  (inf  m)  m)  \mdiv{}  4
                            ,  \mlambda{}k.((inf  (4  *  k))  +  1)
                            ,  \mlambda{}k.eval  a@0  =  inf  (2  *  k)  in
                                      eval  b  =  (inf  (4  *  2  *  k))  +  1  in
                                          if  (b)  <  (a@0)    then  a@0    else  b>

---

Home Index