---

Step * of Lemma rabs-Riemann-integral

∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].  (|∫ f[x] dx on [a, b]| ≤ (||f[x]||_x:[a, b] * (b - a)\000C))
BY
{ (InstLemma  `Riemann-integral-bounds` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (Unhide THENA Auto)
   THEN InstHyp [⌜-(||f[x]||_x:[a, b])⌝;⌜||f[x]||_x:[a, b]⌝] (-1)⋅
   THEN Auto) }

1
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. ∀c1,c2:ℝ.
     ((c1 * (b - a)) ≤ ∫ f[x] dx on [a, b]) ∧ (∫ f[x] dx on [a, b] ≤ (c2 * (b - a))) 
     supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((c1 ≤ f[x]) ∧ (f[x] ≤ c2)))
5. x : ℝ
6. x ∈ [a, b]
⊢ -(||f[x]||_x:[a, b]) ≤ f[x]

2
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. ∀c1,c2:ℝ.
     ((c1 * (b - a)) ≤ ∫ f[x] dx on [a, b]) ∧ (∫ f[x] dx on [a, b] ≤ (c2 * (b - a))) 
     supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((c1 ≤ f[x]) ∧ (f[x] ≤ c2)))
5. x : ℝ
6. x ∈ [a, b]
7. -(||f[x]||_x:[a, b]) ≤ f[x]
⊢ f[x] ≤ ||f[x]||_x:[a, b]

3
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. f : {f:[a, b] ⟶ℝ| ifun(f;[a, b])} 
4. ∀c1,c2:ℝ.
     ((c1 * (b - a)) ≤ ∫ f[x] dx on [a, b]) ∧ (∫ f[x] dx on [a, b] ≤ (c2 * (b - a))) 
     supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((c1 ≤ f[x]) ∧ (f[x] ≤ c2)))
5. (-(||f[x]||_x:[a, b]) * (b - a)) ≤ ∫ f[x] dx on [a, b]
6. ∫ f[x] dx on [a, b] ≤ (||f[x]||_x:[a, b] * (b - a))
⊢ |∫ f[x] dx on [a, b]| ≤ (||f[x]||_x:[a, b] * (b - a))

---

Latex:

---

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[b:\{b:\mBbbR{}|  a  \mleq{}  b\}  ].  \mforall{}[f:\{f:[a,  b]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  b])\}  ].
    (|\mint{}  f[x]  dx  on  [a,  b]|  \mleq{}  (||f[x]||\_x:[a,  b]  *  (b  -  a)))


By

---

Latex:
(InstLemma    `Riemann-integral-bounds`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (Unhide  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}-(||f[x]||\_x:[a,  b])\mkleeneclose{};\mkleeneopen{}||f[x]||\_x:[a,  b]\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index