Step
*
1
1
1
2
of Lemma
cantor-to-interval-req
1. v : ℝ
2. lim n→∞.v * (r(2)/r(3))^n = r0
⊢ lim n→∞.(2^n * v)/3^n = r0
BY
{ TACTIC:(MoveToConcl (-1) THEN BLemma `converges-to_functionality`  THEN Auto) }
1
1. v : ℝ
2. n : ℕ
⊢ (v * (r(2)/r(3))^n) = (2^n * v)/3^n
Latex:
Latex:
1.  v  :  \mBbbR{}
2.  lim  n\mrightarrow{}\minfty{}.v  *  (r(2)/r(3))\^{}n  =  r0
\mvdash{}  lim  n\mrightarrow{}\minfty{}.(2\^{}n  *  v)/3\^{}n  =  r0
By
Latex:
TACTIC:(MoveToConcl  (-1)  THEN  BLemma  `converges-to\_functionality`    THEN  Auto)
Home
Index