---

Step * of Lemma partition-sum_functionality

∀I:Interval
  (icompact(I)
  ⇒ (∀p:partition(I). ∀q:ℝ List.
        ((||q|| = ||p|| ∈ ℤ)
        ⇒ (∀i:ℕ||q||. (q[i] = p[i]))
        ⇒ (∀f:I ⟶ℝ. ∀x:partition-choice(full-partition(I;p)).
              (S(f;full-partition(I;p)) = S(f;full-partition(I;q)))))))
BY
{ xxx(Auto
      THEN RepUR ``partition-sum`` 0
      THEN ((Assert ⌜||full-partition(I;q)|| = ||full-partition(I;p)|| ∈ ℤ⌝⋅
             THENA (RepUR ``full-partition`` 0 THEN Auto')
             )
      THENM HypSubst' (-1) 0
      ))xxx }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. q : ℝ List
5. ||q|| = ||p|| ∈ ℤ
6. ∀i:ℕ||q||. (q[i] = p[i])
7. f : I ⟶ℝ
8. x : partition-choice(full-partition(I;p))
9. ||full-partition(I;q)|| = ||full-partition(I;p)|| ∈ ℤ
⊢ Σ{(f (x i)) * (full-partition(I;p)[i + 1] - full-partition(I;p)[i]) | 0≤i≤||full-partition(I;p)|| - 2}
= Σ{(f (x i)) * (full-partition(I;q)[i + 1] - full-partition(I;q)[i]) | 0≤i≤||full-partition(I;p)|| - 2}

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}p:partition(I).  \mforall{}q:\mBbbR{}  List.
                ((||q||  =  ||p||)
                {}\mRightarrow{}  (\mforall{}i:\mBbbN{}||q||.  (q[i]  =  p[i]))
                {}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}x:partition-choice(full-partition(I;p)).
                            (S(f;full-partition(I;p))  =  S(f;full-partition(I;q)))))))


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``partition-sum``  0
        THEN  ((Assert  \mkleeneopen{}||full-partition(I;q)||  =  ||full-partition(I;p)||\mkleeneclose{}\mcdot{}
                      THENA  (RepUR  ``full-partition``  0  THEN  Auto')
                      )
        THENM  HypSubst'  (-1)  0
        ))xxx

---

Home Index