---

Step * 1 of Lemma uniform-partition-refines


1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. k : ℕ+
4. m : ℕ+
5. icompact([a, b])
6. i : ℕk - 1
⊢ (∃y∈uniform-partition([a, b];m * k). uniform-partition([a, b];k)[i] = y)
BY
{ ((Assert 1 ≤ m BY
          Auto)
   THEN Mul ⌜i + 1⌝ (-1)⋅
   THEN Auto
   THEN (Assert i + 1 < k BY
               Auto)
   THEN Mul ⌜m⌝ (-1)⋅
   THEN With ⌜(m * (i + 1)) - 1⌝ (D 0)⋅
   THEN Auto
   THEN Unfold `uniform-partition` 0
   THEN RWO "mklist_length mklist_select" 0
   THEN Auto
   THEN Reduce 0) }

1
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. k : ℕ+
4. m : ℕ+
5. icompact([a, b])
6. i : ℕk - 1
7. 1 ≤ m
8. ((i + 1) * 1) ≤ ((i + 1) * m)
9. i + 1 < k
10. m * (i + 1) < m * k
⊢ (((r(k) - r(i + 1)) * a) + (r(i + 1) * b)/r(k))
= (((r(m * k) - r(((m * (i + 1)) - 1) + 1)) * a) + (r(((m * (i + 1)) - 1) + 1) * b)/r(m * k))

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \{b:\mBbbR{}|  a  \mleq{}  b\} 
3.  k  :  \mBbbN{}\msupplus{}
4.  m  :  \mBbbN{}\msupplus{}
5.  icompact([a,  b])
6.  i  :  \mBbbN{}k  -  1
\mvdash{}  (\mexists{}y\mmember{}uniform-partition([a,  b];m  *  k).  uniform-partition([a,  b];k)[i]  =  y)


By

---

Latex:
((Assert  1  \mleq{}  m  BY
                Auto)
  THEN  Mul  \mkleeneopen{}i  +  1\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto
  THEN  (Assert  i  +  1  <  k  BY
                          Auto)
  THEN  Mul  \mkleeneopen{}m\mkleeneclose{}  (-1)\mcdot{}
  THEN  With  \mkleeneopen{}(m  *  (i  +  1))  -  1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Unfold  `uniform-partition`  0
  THEN  RWO  "mklist\_length  mklist\_select"  0
  THEN  Auto
  THEN  Reduce  0)

---

Home Index