---

Step * 1 of Lemma integral-single


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)
BY
{ (Auto THEN Unfold `integral` 0 THEN RWO "Riemann-integral-single" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [a]  :  \mBbbR{}
2.  a  \mleq{}  rmin(a;a)
3.  rmax(a;a)  \mleq{}  a
\mvdash{}  \mforall{}[f:\{f:[a,  a]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[a,  a])\}  ].  (a\_\mint{}\msupminus{}a  f[x]  dx  =  r0)


By

---

Latex:
(Auto  THEN  Unfold  `integral`  0  THEN  RWO  "Riemann-integral-single"  0  THEN  Auto)

---

Home Index