---

Step * 1 of Lemma real-from-approx_wf


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} 
BY
{ ((InstLemma `req-from-converges`  [⌜λ2n.x[n + 1]⌝;⌜a⌝;⌜λk.k⌝]⋅ THENA Auto) THEN Reduce -1) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  x  :  k:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{v:\mBbbR{}|  |v  -  a|  \mleq{}  (r1/r(k))\} 
3.  \mlambda{}k.k  \mmember{}  lim  n\mrightarrow{}\minfty{}.x[n  +  1]  =  a
\mvdash{}  real-from-approx(n.x[n])  \mmember{}  \{b:\mBbbR{}|  b  =  a\} 


By

---

Latex:
((InstLemma  `req-from-converges`    [\mkleeneopen{}\mlambda{}\msubtwo{}n.x[n  +  1]\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}\mlambda{}k.k\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  Reduce  -1)

---

Home Index