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


1. : ℝ
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. : ℝ
2. : ℕ
⊢ (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