---

Step * of Lemma integral-equal-endpoints

∀I:Interval. ∀f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} . ∀a,b:{a:ℝ| a ∈ I} .
  ((a = b) ⇒ (a_∫-b f[t] dt = r0))
BY
{ (InstLemma `integral-same-endpoints` [] THEN RepeatFor 3 (ParallelLast') THEN Auto) }

1
1. I : Interval
2. f : {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ ((f x) = (f y)))} 
3. a : {a:ℝ| a ∈ I} 
4. a_∫-a f[t] dt = r0
5. b : {a:ℝ| a ∈ I} 
6. a = b
⊢ a_∫-b f[t] dt = r0

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}f:\{f:I  {}\mrightarrow{}\mBbbR{}|  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  ((f  x)  =  (f  y)))\}  .  \mforall{}a,b:\{a:\mBbbR{}|  a  \mmember{}  I\}  .
    ((a  =  b)  {}\mRightarrow{}  (a\_\mint{}\msupminus{}b  f[t]  dt  =  r0))


By

---

Latex:
(InstLemma  `integral-same-endpoints`  []  THEN  RepeatFor  3  (ParallelLast')  THEN  Auto)

---

Home Index