---

Step * 1 of Lemma integral_functionality_endpoints


1. a : ℝ
2. b : ℝ
3. f : {f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} 
4. a' : ℝ
5. b' : ℝ
6. b = b'
7. a = a'
⊢ a_∫-b f[x] dx = a'_∫-b' f[x] dx
BY
{ (Unfold `integral` 0 THEN RWO "6 7" 0 THEN Auto THEN Try ((RWO "6 7" 0 THEN Auto))) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  f  :  \{f:[rmin(a;b),  rmax(a;b)]  {}\mrightarrow{}\mBbbR{}|  ifun(f;[rmin(a;b),  rmax(a;b)])\} 
4.  a'  :  \mBbbR{}
5.  b'  :  \mBbbR{}
6.  b  =  b'
7.  a  =  a'
\mvdash{}  a\_\mint{}\msupminus{}b  f[x]  dx  =  a'\_\mint{}\msupminus{}b'  f[x]  dx


By

---

Latex:
(Unfold  `integral`  0  THEN  RWO  "6  7"  0  THEN  Auto  THEN  Try  ((RWO  "6  7"  0  THEN  Auto)))

---

Home Index