---

Step * of Lemma real-from-approx_wf

∀[a:ℝ]. ∀[x:k:ℕ+ ⟶ {v:ℝ| |v - a| ≤ (r1/r(k))} ].  (real-from-approx(n.x[n]) ∈ {b:ℝ| b = a} )
BY
{ (Auto
   THEN (Assert λk.k ∈ lim n→∞.x[n + 1] = a BY
               (RepUR ``converges-to all`` 0
                THEN (MemCD THENA Auto)
                THEN MemTypeCD
                THEN Auto
                THEN (GenConclTerm ⌜x[n + 1]⌝⋅ THENA Auto)
                THEN D -2
                THEN (Unhide THENA Auto)
                THEN RWO "-2" 0
                THEN Auto))
   ) }

1
1. a : ℝ
2. x : k:ℕ+ ⟶ {v:ℝ| |v - a| ≤ (r1/r(k))} 
3. λk.k ∈ lim n→∞.x[n + 1] = a
⊢ real-from-approx(n.x[n]) ∈ {b:ℝ| b = a} 

---

Latex:

---

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[x:k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{v:\mBbbR{}|  |v  -  a|  \mleq{}  (r1/r(k))\}  ].    (real-from-approx(n.x[n])  \mmember{}  \{b:\mBbbR{}|  b  =  a\}  )


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}k.k  \mmember{}  lim  n\mrightarrow{}\minfty{}.x[n  +  1]  =  a  BY
                          (RepUR  ``converges-to  all``  0
                            THEN  (MemCD  THENA  Auto)
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  (GenConclTerm  \mkleeneopen{}x[n  +  1]\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  (Unhide  THENA  Auto)
                            THEN  RWO  "-2"  0
                            THEN  Auto))
  )

---

Home Index