---

Step * of Lemma uniform-partition-point

∀[I:Interval]
  ∀[k:ℕ+]
    ∀i:ℕk + 1
      ((full-partition(I;uniform-partition(I;k))[i] * r(k))
      = (((r(k) - r(i)) * left-endpoint(I)) + (r(i) * right-endpoint(I)))) 
  supposing icompact(I)
BY
{ (Auto
   THEN RepUR ``full-partition uniform-partition`` 0
   THEN (RWW "length-append mklist_length" 0 THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN CaseNat 0 `i'
   THEN Reduce 0) }

1
1. I : Interval
2. icompact(I)
3. k : ℕ+
4. i : ℕk + 1
5. i = 0 ∈ ℤ
⊢ (left-endpoint(I) * r(k)) = (((r(k) - r0) * left-endpoint(I)) + (r0 * right-endpoint(I)))

2
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)))

---

Latex:

---

Latex:
\mforall{}[I:Interval]
    \mforall{}[k:\mBbbN{}\msupplus{}]
        \mforall{}i:\mBbbN{}k  +  1
            ((full-partition(I;uniform-partition(I;k))[i]  *  r(k))
            =  (((r(k)  -  r(i))  *  left-endpoint(I))  +  (r(i)  *  right-endpoint(I)))) 
    supposing  icompact(I)


By

---

Latex:
(Auto
  THEN  RepUR  ``full-partition  uniform-partition``  0
  THEN  (RWW  "length-append  mklist\_length"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  CaseNat  0  `i'
  THEN  Reduce  0)

---

Home Index