---

Step * of Lemma rabs-integral

∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
  (|a_∫-b f[x] dx| ≤ (||f[x]||_x:[rmin(a;b), rmax(a;b)] * |a - b|))
BY
{ (Auto
   THEN (Assert rmin(a;b) ≤ rmin(rmin(a;b);rmax(a;b)) BY
               (BLemma `rmin_ub` THEN Auto))
   THEN (Assert rmax(rmin(a;b);rmax(a;b)) ≤ rmax(a;b) BY
               (BLemma `rmax_lb` THEN Auto))
   THEN Assert ⌜|a_∫-b f[x] dx| ≤ |rmin(a;b)_∫-rmax(a;b) f[x] dx|⌝⋅) }

1
.....assertion..... 
1. a : ℝ
2. b : ℝ
3. f : {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} 
4. rmin(a;b) ≤ rmin(rmin(a;b);rmax(a;b))
5. rmax(rmin(a;b);rmax(a;b)) ≤ rmax(a;b)
⊢ |a_∫-b f[x] dx| ≤ |rmin(a;b)_∫-rmax(a;b) f[x] dx|

2
1. a : ℝ
2. b : ℝ
3. f : {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} 
4. rmin(a;b) ≤ rmin(rmin(a;b);rmax(a;b))
5. rmax(rmin(a;b);rmax(a;b)) ≤ rmax(a;b)
6. |a_∫-b f[x] dx| ≤ |rmin(a;b)_∫-rmax(a;b) f[x] dx|
⊢ |a_∫-b f[x] dx| ≤ (||f[x]||_x:[rmin(a;b), rmax(a;b)] * |a - b|)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  rmin(a;b)  \mleq{}  rmin(rmin(a;b);rmax(a;b))  BY
                          (BLemma  `rmin\_ub`  THEN  Auto))
  THEN  (Assert  rmax(rmin(a;b);rmax(a;b))  \mleq{}  rmax(a;b)  BY
                          (BLemma  `rmax\_lb`  THEN  Auto))
  THEN  Assert  \mkleeneopen{}|a\_\mint{}\msupminus{}b  f[x]  dx|  \mleq{}  |rmin(a;b)\_\mint{}\msupminus{}rmax(a;b)  f[x]  dx|\mkleeneclose{}\mcdot{})

---

Home Index