---

Step * 2 of Lemma uniform-partition-point


1. I : Interval
2. icompact(I)
3. k : ℕ+
4. i : ℕk + 1
5. ¬(i = 0 ∈ ℤ)
⊢ ([left-endpoint(I) / 
    (mklist(k - 1;λi.(((r(k) - r(i + 1)) * left-endpoint(I)) + (r(i + 1) * right-endpoint(I))/r(k)))
    @ [right-endpoint(I)])][i]
* r(k))
= (((r(k) - r(i)) * left-endpoint(I)) + (r(i) * right-endpoint(I)))
BY
{ ((Assert r(k) ≠ r0 BY
          Auto)
   THEN (RWO "select_cons_tl" 0
         THENA (Auto THEN ((RWW "length-append mklist_length" 0 THENA Auto) THEN Reduce 0 THEN Auto)⋅)
         )
   THEN (Decide ⌜i = k ∈ ℤ⌝⋅ THENA Auto))⋅ }

1
1. I : Interval
2. icompact(I)
3. k : ℕ+
4. i : ℕk + 1
5. ¬(i = 0 ∈ ℤ)
6. r(k) ≠ r0
7. i = k ∈ ℤ
⊢ (mklist(k - 1;λi.(((r(k) - r(i + 1)) * left-endpoint(I)) + (r(i + 1) * right-endpoint(I))/r(k)))
@ [right-endpoint(I)][i - 1]
* r(k))
= (((r(k) - r(i)) * left-endpoint(I)) + (r(i) * right-endpoint(I)))

2
1. I : Interval
2. icompact(I)
3. k : ℕ+
4. i : ℕk + 1
5. ¬(i = 0 ∈ ℤ)
6. r(k) ≠ r0
7. ¬(i = k ∈ ℤ)
⊢ (mklist(k - 1;λi.(((r(k) - r(i + 1)) * left-endpoint(I)) + (r(i + 1) * right-endpoint(I))/r(k)))
@ [right-endpoint(I)][i - 1]
* r(k))
= (((r(k) - r(i)) * left-endpoint(I)) + (r(i) * right-endpoint(I)))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  k  :  \mBbbN{}\msupplus{}
4.  i  :  \mBbbN{}k  +  1
5.  \mneg{}(i  =  0)
\mvdash{}  ([left-endpoint(I)  / 
        (mklist(k  -  1;\mlambda{}i.(((r(k)  -  r(i  +  1))  *  left-endpoint(I))  +  (r(i  +  1)  *  right-endpoint(I))/r(k)))
        @  [right-endpoint(I)])][i]
*  r(k))
=  (((r(k)  -  r(i))  *  left-endpoint(I))  +  (r(i)  *  right-endpoint(I)))


By

---

Latex:
((Assert  r(k)  \mneq{}  r0  BY
                Auto)
  THEN  (RWO  "select\_cons\_tl"  0
              THENA  (Auto  THEN  ((RWW  "length-append  mklist\_length"  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)\mcdot{})
              )
  THEN  (Decide  \mkleeneopen{}i  =  k\mkleeneclose{}\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index