---

Step * 1 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
4. a = cauchy-limit(n.x[n + 1];λk.(2 * k))
⊢ real-from-approx(n.x[n]) ∈ {b:ℝ| b = a} 
BY
{ (Assert ⌜real-from-approx(n.x[n]) ∈ ℝ⌝⋅
THENM ((Subst' cauchy-limit(n.x[n + 1];λk.(2 * k)) ~ real-from-approx(n.x[n]) -2
        THENA (Unfold `real-from-approx` 0 THEN EqCD)
        )
       THEN Auto
       )
) }

1
.....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]) ∈ ℝ

---

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


By

---

Latex:
(Assert  \mkleeneopen{}real-from-approx(n.x[n])  \mmember{}  \mBbbR{}\mkleeneclose{}\mcdot{}
THENM  ((Subst'  cauchy-limit(n.x[n  +  1];\mlambda{}k.(2  *  k))  \msim{}  real-from-approx(n.x[n])  -2
                THENA  (Unfold  `real-from-approx`  0  THEN  EqCD)
                )
              THEN  Auto
              )
)

---

Home Index