---

Step * 1 1 1 1 1 of Lemma cantor-to-interval-req

.....assertion..... 
1. v : ℝ
2. lim n→∞.v = v
⊢ lim n→∞.(r(2)/r(3))^n = r0
BY
{ TACTIC:(BLemma `rnexp-converges-ext` THEN Auto THEN (RWO "rabs-of-nonneg" 0 THEN Auto)⋅) }

---

Latex:

---

Latex:
.....assertion..... 
1.  v  :  \mBbbR{}
2.  lim  n\mrightarrow{}\minfty{}.v  =  v
\mvdash{}  lim  n\mrightarrow{}\minfty{}.(r(2)/r(3))\^{}n  =  r0


By

---

Latex:
TACTIC:(BLemma  `rnexp-converges-ext`  THEN  Auto  THEN  (RWO  "rabs-of-nonneg"  0  THEN  Auto)\mcdot{})

---

Home Index