Step * of Lemma Riemann-sums-converge

a:ℝ. ∀b:{b:ℝa ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum(f;a;b;k 1)↓ as k→∞
BY
(Auto THEN BLemma `converges-iff-cauchy` THEN Auto THEN THEN Auto) }

1
1. : ℝ
2. {b:ℝa ≤ b} 
3. [a, b] ⟶ℝ
4. mc f[x] continuous for x ∈ [a, b]
5. k@0 : ℕ+
⊢ ∃N:{ℕ(∀k,m:ℕ.  ((N ≤ k)  (N ≤ m)  (|Riemann-sum(f;a;b;k 1) Riemann-sum(f;a;b;m 1)| ≤ (r1/r(k@0)))))}


Latex:


Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}f:[a,  b]  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  [a,  b].
    Riemann-sum(f;a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}


By


Latex:
(Auto  THEN  BLemma  `converges-iff-cauchy`  THEN  Auto  THEN  D  0  THEN  Auto)




Home Index