### Nuprl 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))`

Proof

Definitions occuring in Statement :  Riemann-sum: `Riemann-sum(f;a;b;k)` continuous: `f[x] continuous for x ∈ I` rfun: `I ⟶ℝ` rccint: `[l, u]` cauchy: `cauchy(n.x[n])` rleq: `x ≤ y` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` set: `{x:A| B[x]} ` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  subtype_rel: `A ⊆r B` so_apply: `x[s]` rfun: `I ⟶ℝ` label: `...\$L... t` so_lambda: `λ2x.t[x]` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T` cauchy: `cauchy(n.x[n])` all: `∀x:A. B[x]` top: `Top` not: `¬A` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` decidable: `Dec(P)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` cand: `A c∧ B` or: `P ∨ Q` nat_plus: `ℕ+` squash: `↓T` uimplies: `b supposing a` rev_uimplies: `rev_uimplies(P;Q)` and: `P ∧ Q` uiff: `uiff(P;Q)` implies: `P `` Q` sq_stable: `SqStable(P)` rsub: `x - y` sq_exists: `∃x:{A| B[x]}` rless: `x < y` guard: `{T}` rneq: `x ≠ y` i-member: `r ∈ I` rccint: `[l, u]` i-approx: `i-approx(I;n)` true: `True` less_than': `less_than'(a;b)` less_than: `a < b` continuous: `f[x] continuous for x ∈ I` rleq: `x ≤ y` rnonneg: `rnonneg(x)` le: `A ≤ B` ge: `i ≥ j ` subtract: `n - m` real: `ℝ` nat: `ℕ` rge: `x ≥ y` i-length: `|I|`
Rules used in proof :  setEquality applyEquality lambdaEquality sqequalRule setElimination hypothesisEquality thin isectElimination sqequalHypSubstitution hypothesis lemma_by_obid cut rename lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution computeAll independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation unionElimination dependent_functionElimination inlFormation multiplyEquality imageElimination baseClosed imageMemberEquality independent_isectElimination productElimination because_Cache introduction independent_functionElimination natural_numberEquality minusEquality equalitySymmetry equalityTransitivity inrFormation functionEquality productEquality dependent_set_memberEquality independent_pairEquality axiomEquality dependent_set_memberFormation addEquality promote_hyp isect_memberFormation equalityEquality

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))

Date html generated: 2016_05_18-AM-10_42_44
Last ObjectModification: 2016_01_17-AM-00_32_09

Theory : reals

Home Index