---

Step * of Lemma integral-zero

∀[a,b:ℝ].  (a_∫-b r0 dx = r0)
BY
{ (InstLemma `integral-const` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D -1 With ⌜r0⌝  THENA Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbR{}].    (a\_\mint{}\msupminus{}b  r0  dx  =  r0)


By

---

Latex:
(InstLemma  `integral-const`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  -1  With  \mkleeneopen{}r0\mkleeneclose{}    THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index