---

Step * of Lemma mesh-uniform-partition

∀[I:Interval]. ∀[k:ℕ+]. (partition-mesh(I;uniform-partition(I;k)) = (|I|/r(k))) supposing icompact(I)
BY
{ (Auto
   THEN Unfold `partition-mesh` 0
   THEN Unfold `frs-mesh` 0
   THEN ((SplitOnConclITE THENA Auto)
         THENL [(RepUR ``full-partition`` (-1) THEN Auto')
               ; (BLemma `rmaximum-constant`
                  THEN Auto
                  THEN (Assert ||full-partition(I;uniform-partition(I;k))|| = (k + 1) ∈ ℤ BY
                              (RepUR ``full-partition`` 0⋅
                               THEN (RWW "length-append" 0 THENA Auto)
                               THEN RepUR ``uniform-partition`` 0
                               THEN (RWO "mklist_length" 0 THENA Auto)
                               THEN Auto)⋅)
                  THEN (Assert i < k BY
                              Auto')
                  THEN (nRMul ⌜r(k)⌝ 0⋅ THEN Auto)⋅)]
   )) }

1
1. I : Interval
2. icompact(I)
3. k : ℕ+
4. 2 ≤ ||full-partition(I;uniform-partition(I;k))||
5. i : ℕ(||full-partition(I;uniform-partition(I;k))|| - 2) + 1
6. ||full-partition(I;uniform-partition(I;k))|| = (k + 1) ∈ ℤ
7. i < k
⊢ ((r(k) * full-partition(I;uniform-partition(I;k))[i + 1]) + -(r(k) * full-partition(I;uniform-partition(I;k))[i]))
= |I|

---

Latex:

---

Latex:
\mforall{}[I:Interval]
    \mforall{}[k:\mBbbN{}\msupplus{}].  (partition-mesh(I;uniform-partition(I;k))  =  (|I|/r(k)))  supposing  icompact(I)


By

---

Latex:
(Auto
  THEN  Unfold  `partition-mesh`  0
  THEN  Unfold  `frs-mesh`  0
  THEN  ((SplitOnConclITE  THENA  Auto)
              THENL  [(RepUR  ``full-partition``  (-1)  THEN  Auto')
                          ;  (BLemma  `rmaximum-constant`
                                THEN  Auto
                                THEN  (Assert  ||full-partition(I;uniform-partition(I;k))||  =  (k  +  1)  BY
                                                        (RepUR  ``full-partition``  0\mcdot{}
                                                          THEN  (RWW  "length-append"  0  THENA  Auto)
                                                          THEN  RepUR  ``uniform-partition``  0
                                                          THEN  (RWO  "mklist\_length"  0  THENA  Auto)
                                                          THEN  Auto)\mcdot{})
                                THEN  (Assert  i  <  k  BY
                                                        Auto')
                                THEN  (nRMul  \mkleeneopen{}r(k)\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{})]
  ))

---

Home Index