---

Step * of Lemma integral-single

∀[a:ℝ]. ∀[f:{f:[a, a] ⟶ℝ| ifun(f;[a, a])} ].  (a_∫-a f[x] dx = r0)
BY
{ (Intro
   THEN (Assert a ≤ rmin(a;a) BY
               ((Unhide THENA Auto) THEN BLemma `rmin_ub` THEN Auto))
   THEN (Assert rmax(a;a) ≤ a BY
               ((Unhide THENA Auto) THEN BLemma `rmax_lb` THEN Auto))) }

1
1. [a] : ℝ
2. a ≤ rmin(a;a)
3. rmax(a;a) ≤ a
⊢ ∀[f:{f:[a, a] ⟶ℝ| ifun(f;[a, a])} ]. (a_∫-a f[x] dx = r0)

---

Latex:

---

Latex:
\mforall{}[a:\mBbbR{}].  \mforall{}[f:\{f:[a,  a]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  a])\}  ].    (a\_\mint{}\msupminus{}a  f[x]  dx  =  r0)


By

---

Latex:
(Intro
  THEN  (Assert  a  \mleq{}  rmin(a;a)  BY
                          ((Unhide  THENA  Auto)  THEN  BLemma  `rmin\_ub`  THEN  Auto))
  THEN  (Assert  rmax(a;a)  \mleq{}  a  BY
                          ((Unhide  THENA  Auto)  THEN  BLemma  `rmax\_lb`  THEN  Auto)))

---

Home Index