### Nuprl Lemma : alt-Riemann-sums-cauchy

`∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b].  cauchy(k.Riemann-sum-alt(f;a;b;k + 1))`

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]` 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 :  rfun: `I ⟶ℝ` label: `...\$L... t` so_apply: `x[s]` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` guard: `{T}` rneq: `x ≠ y` true: `True` less_than': `less_than'(a;b)` top: `Top` subtype_rel: `A ⊆r B` subtract: `n - m` uimplies: `b supposing a` uiff: `uiff(P;Q)` false: `False` rev_implies: `P `` Q` not: `¬A` iff: `P `⇐⇒` Q` or: `P ∨ Q` decidable: `Dec(P)` and: `P ∧ Q` le: `A ≤ B` nat_plus: `ℕ+` so_lambda: `λ2x.t[x]` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` implies: `P `` Q` sq_exists: `∃x:{A| B[x]}` cauchy: `cauchy(n.x[n])` member: `t ∈ T` all: `∀x:A. B[x]` rev_uimplies: `rev_uimplies(P;Q)` cand: `A c∧ B` rccint: `[l, u]` i-member: `r ∈ I`
Lemmas referenced :  and_wf continuous-implies-functional member_rccint_lemma req_inversion req_weakening Riemann-sum-alt-req rsub_functionality rabs_functionality rleq_functionality Riemann-sums-cauchy le_wf nat_wf all_wf rleq_wf rabs_wf rsub_wf Riemann-sum-alt_wf decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel less_than_wf rdiv_wf int-to-real_wf rless-int nat_properties nat_plus_properties satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf rless_wf nat_plus_wf continuous_wf rccint_wf subtype_rel_self rfun_wf real_wf i-member_wf Riemann-sum_wf req_wf
Rules used in proof :  setEquality computeAll int_eqEquality dependent_pairFormation inrFormation minusEquality intEquality voidEquality isect_memberEquality applyEquality independent_isectElimination voidElimination independent_pairFormation unionElimination productElimination natural_numberEquality addEquality functionEquality because_Cache lambdaEquality sqequalRule isectElimination independent_functionElimination dependent_set_memberEquality introduction rename setElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution lemma_by_obid cut addLevel levelHypothesis promote_hyp andLevelFunctionality

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-alt(f;a;b;k  +  1))

Date html generated: 2016_05_18-AM-10_45_55
Last ObjectModification: 2016_01_17-AM-00_22_33

Theory : reals

Home Index