---

Step * 1 1 1 of Lemma real-from-approx_wf

.....assertion..... 
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]) ∈ ℝ
BY
{ ((Unfold `real-from-approx` 0 THEN MemCD) THEN Try (Complete (Auto))) }

1
.....subterm..... T:t
2:n
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))
⊢ λk.(2 * k) ∈ cauchy(n.x[n + 1])

---

Latex:

---

Latex:
.....assertion..... 
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
4.  a  =  cauchy-limit(n.x[n  +  1];\mlambda{}k.(2  *  k))
\mvdash{}  real-from-approx(n.x[n])  \mmember{}  \mBbbR{}


By

---

Latex:
((Unfold  `real-from-approx`  0  THEN  MemCD)  THEN  Try  (Complete  (Auto)))

---

Home Index