Step
*
of Lemma
comparison-test
No Annotations
∀y:ℕ ⟶ ℝ. (Σn.y[n]↓
⇒ (∀x:ℕ ⟶ ℝ. Σn.x[n]↓ supposing ∀n:ℕ. (|x[n]| ≤ y[n])))
BY
{ TACTIC:(Auto
THEN All (RepUR ``series-converges series-sum``)
THEN All (Fold `converges`)
THEN All (RWO "converges-iff-cauchy-ext")
THEN Auto) }
1
1. y : ℕ ⟶ ℝ@i
2. cauchy(n.Σ{y[i] | 0≤i≤n})
3. x : ℕ ⟶ ℝ@i
4. ∀n:ℕ. (|x[n]| ≤ y[n])
⊢ cauchy(n.Σ{x[i] | 0≤i≤n})
Latex:
Latex:
No Annotations
\mforall{}y:\mBbbN{} {}\mrightarrow{} \mBbbR{}. (\mSigma{}n.y[n]\mdownarrow{} {}\mRightarrow{} (\mforall{}x:\mBbbN{} {}\mrightarrow{} \mBbbR{}. \mSigma{}n.x[n]\mdownarrow{} supposing \mforall{}n:\mBbbN{}. (|x[n]| \mleq{} y[n])))
By
Latex:
TACTIC:(Auto
THEN All (RepUR ``series-converges series-sum``)
THEN All (Fold `converges`)
THEN All (RWO "converges-iff-cauchy-ext")
THEN Auto)
Home
Index