Step
*
of Lemma
Riemann-sums-cauchy
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  cauchy(k.Riemann-sum(f;a;b;k + 1))
BY
{ (Auto THEN D 0 THEN Auto THEN RenameVar `n' (-1)) }
1
1. a : ℝ@i
2. b : {b:ℝ| a ≤ b} @i
3. f : [a, b] ⟶ℝ@i
4. mc : f[x] continuous for x ∈ [a, b]@i
5. n : ℕ+@i
⊢ ∃N:{ℕ| (∀k,m:ℕ.  ((N ≤ k) 
⇒ (N ≤ m) 
⇒ (|Riemann-sum(f;a;b;k + 1) - Riemann-sum(f;a;b;m + 1)| ≤ (r1/r(n)))))}
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].
    cauchy(k.Riemann-sum(f;a;b;k  +  1))
By
Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  RenameVar  `n'  (-1))
Home
Index