Step
*
1
of Lemma
common-limit-squeeze
.....assertion.....
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. c : ℕ ⟶ ℝ
4. ∀n:ℕ. ((a[n] ≤ a[n + 1]) ∧ (a[n + 1] ≤ b[n + 1]) ∧ (b[n + 1] ≤ b[n]))
5. lim n→∞.c[n] = r0
6. ∀n:ℕ. r0≤b[n] - a[n]≤c[n]
⊢ ∃y:ℝ. lim n→∞.a[n] = y
BY
{ (Fold `converges` 0 THEN BLemma `converges-iff-cauchy` THEN Auto) }
1
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. c : ℕ ⟶ ℝ
4. ∀n:ℕ. ((a[n] ≤ a[n + 1]) ∧ (a[n + 1] ≤ b[n + 1]) ∧ (b[n + 1] ≤ b[n]))
5. lim n→∞.c[n] = r0
6. ∀n:ℕ. r0≤b[n] - a[n]≤c[n]
⊢ cauchy(n.a[n])
Latex:
Latex:
.....assertion.....
1. a : \mBbbN{} {}\mrightarrow{} \mBbbR{}
2. b : \mBbbN{} {}\mrightarrow{} \mBbbR{}
3. c : \mBbbN{} {}\mrightarrow{} \mBbbR{}
4. \mforall{}n:\mBbbN{}. ((a[n] \mleq{} a[n + 1]) \mwedge{} (a[n + 1] \mleq{} b[n + 1]) \mwedge{} (b[n + 1] \mleq{} b[n]))
5. lim n\mrightarrow{}\minfty{}.c[n] = r0
6. \mforall{}n:\mBbbN{}. r0\mleq{}b[n] - a[n]\mleq{}c[n]
\mvdash{} \mexists{}y:\mBbbR{}. lim n\mrightarrow{}\minfty{}.a[n] = y
By
Latex:
(Fold `converges` 0 THEN BLemma `converges-iff-cauchy` THEN Auto)
Home
Index