Nuprl Lemma : alt-Riemann-sums-converge-ext

a:ℝ. ∀b:{b:ℝa ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  Riemann-sum-alt(f;a;b;k 1)↓ as k→∞


Proof




Definitions occuring in Statement :  Riemann-sum-alt: Riemann-sum-alt(f;a;b;k) continuous: f[x] continuous for x ∈ I rfun: I ⟶ℝ rccint: [l, u] converges: x[n]↓ as n→∞ rleq: x ≤ y real: so_apply: x[s] all: x:A. B[x] set: {x:A| B[x]}  add: m natural_number: $n
Definitions unfolded in proof :  ifthenelse: if then else fi  subtract: m sq_stable__rless sq_stable__and rless-cases integer-bound so_apply: x[s1;s2] so_lambda: λ2y.t[x; y] squash: T or: P ∨ Q guard: {T} prop: has-value: (a)↓ implies:  Q all: x:A. B[x] and: P ∧ Q strict4: strict4(F) uimplies: supposing a top: Top so_apply: x[s1;s2;s3;s4] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) uall: [x:A]. B[x] Riemann-sums-cauchy alt-Riemann-sums-cauchy so_lambda: λ2x.t[x] so_apply: x[s] converges-iff-cauchy alt-Riemann-sums-converge member: t ∈ T
Lemmas referenced :  sq_stable__rless sq_stable__and rless-cases integer-bound Riemann-sums-cauchy alt-Riemann-sums-cauchy converges-iff-cauchy alt-Riemann-sums-converge
Rules used in proof :  inlFormation imageElimination imageMemberEquality intEquality inrFormation exceptionSqequal addExceptionCases equalitySymmetry equalityTransitivity because_Cache productElimination hypothesisEquality closedConclusion baseApply callbyvalueAdd lambdaFormation independent_pairFormation independent_isectElimination voidEquality voidElimination isect_memberEquality baseClosed isectElimination sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

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-alt(f;a;b;k  +  1)\mdownarrow{}  as  k\mrightarrow{}\minfty{}



Date html generated: 2016_07_08-PM-06_00_05
Last ObjectModification: 2016_07_05-PM-03_14_51

Theory : reals


Home Index