---

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

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

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

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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{}  \mlambda{}k.(2  *  k)  \mmember{}  cauchy(n.x[n  +  1])


By

---

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

---

Home Index