### Nuprl Lemma : Riemann-sum-rleq

`∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:[a, b] ⟶ℝ]. ∀[k:ℕ+].`
`  Riemann-sum(f;a;b;k) ≤ Riemann-sum(g;a;b;k) supposing ∀x:ℝ. ((x ∈ [a, b]) `` ((f x) ≤ (g x)))`

Proof

Definitions occuring in Statement :  Riemann-sum: `Riemann-sum(f;a;b;k)` rfun: `I ⟶ℝ` rccint: `[l, u]` i-member: `r ∈ I` rleq: `x ≤ y` real: `ℝ` nat_plus: `ℕ+` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` apply: `f a`
Definitions unfolded in proof :  partition-sum: `partition-sum(f;x;p)` default-partition-choice: `default-partition-choice(p)` nat_plus: `ℕ+` so_apply: `x[s]` rfun: `I ⟶ℝ` so_lambda: `λ2x.t[x]` real: `ℝ` subtype_rel: `A ⊆r B` false: `False` not: `¬A` le: `A ≤ B` rnonneg: `rnonneg(x)` rleq: `x ≤ y` squash: `↓T` Riemann-sum: `Riemann-sum(f;a;b;k)` and: `P ∧ Q` iff: `P `⇐⇒` Q` all: `∀x:A. B[x]` implies: `P `` Q` sq_stable: `SqStable(P)` prop: `ℙ` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` has-value: `(a)↓` callbyvalueall: callbyvalueall has-valueall: `has-valueall(a)` top: `Top` pointwise-rleq: `x[k] ≤ y[k] for k ∈ [n,m]` uiff: `uiff(P;Q)` less_than: `a < b` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` or: `P ∨ Q` decidable: `Dec(P)` lelt: `i ≤ j < k` guard: `{T}` int_seg: `{i..j-}` rccint: `[l, u]` i-member: `r ∈ I` rev_uimplies: `rev_uimplies(P;Q)` rsub: `x - y` frs-non-dec: `frs-non-dec(L)`
Lemmas referenced :  rmul_preserves_rleq2 lelt_wf subtype_rel_list full-partition-non-dec radd-zero-both radd-rminus-both radd_functionality req_weakening radd-ac radd_comm rleq_functionality uiff_transitivity radd-preserves-rleq radd_wf int-to-real_wf rminus_wf equal_wf rsum_functionality_wrt_rleq subtract_wf length_wf rmul_wf select_wf int_seg_properties nat_plus_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf decidable__lt add-is-int-iff subtract-is-int-iff intformless_wf itermAdd_wf itermSubtract_wf int_formula_prop_less_lemma int_term_value_add_lemma int_term_value_subtract_lemma false_wf int_seg_wf le_wf list_set_type full-partition_wf full-partition-point-member member_rccint_lemma uniform-partition_wf partition_wf evalall-reduce sq_stable__rleq Riemann-sum_wf rleq_wf rccint-icompact less_than'_wf rsub_wf real_wf nat_plus_wf all_wf i-member_wf rccint_wf rfun_wf set_wf value-type-has-value set-value-type less_than_wf int-value-type list_wf and_wf valueall-type-has-valueall list-valueall-type set-valueall-type real-valueall-type
Rules used in proof :  equalityEquality lambdaFormation setEquality intEquality independent_isectElimination voidElimination isect_memberEquality functionEquality equalitySymmetry equalityTransitivity axiomEquality natural_numberEquality minusEquality applyEquality independent_pairEquality lambdaEquality imageElimination baseClosed imageMemberEquality sqequalRule productElimination dependent_functionElimination independent_functionElimination because_Cache hypothesis dependent_set_memberEquality hypothesisEquality isectElimination sqequalHypSubstitution lemma_by_obid rename thin setElimination cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution callbyvalueReduce voidEquality closedConclusion baseApply promote_hyp pointwiseFunctionality computeAll independent_pairFormation int_eqEquality dependent_pairFormation unionElimination addEquality productEquality substitution

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[f,g:[a,  b]  {}\mrightarrow{}\mBbbR{}].  \mforall{}[k:\mBbbN{}\msupplus{}].
Riemann-sum(f;a;b;k)  \mleq{}  Riemann-sum(g;a;b;k)  supposing  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  [a,  b])  {}\mRightarrow{}  ((f  x)  \mleq{}  (g  x)))

Date html generated: 2016_05_18-AM-10_40_28
Last ObjectModification: 2016_01_17-AM-00_22_51

Theory : reals

Home Index