Step
*
1
1
1
of Lemma
cantor-to-interval-req
1. v : ℝ
⊢ lim n→∞.(2^n * v)/3^n = r0
BY
{ TACTIC:Assert ⌜lim n→∞.v * (r(2)/r(3))^n = r0⌝⋅ }
1
.....assertion..... 
1. v : ℝ
⊢ lim n→∞.v * (r(2)/r(3))^n = r0
2
1. v : ℝ
2. lim n→∞.v * (r(2)/r(3))^n = r0
⊢ lim n→∞.(2^n * v)/3^n = r0
Latex:
Latex:
1.  v  :  \mBbbR{}
\mvdash{}  lim  n\mrightarrow{}\minfty{}.(2\^{}n  *  v)/3\^{}n  =  r0
By
Latex:
TACTIC:Assert  \mkleeneopen{}lim  n\mrightarrow{}\minfty{}.v  *  (r(2)/r(3))\^{}n  =  r0\mkleeneclose{}\mcdot{}
Home
Index