---

Step * of Lemma uniform-partition-refines

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀k,m:ℕ+.  uniform-partition([a, b];m * k) refines uniform-partition([a, b];k)
BY
{ (Auto
   THEN (Assert icompact([a, b]) BY
               EAuto 1)
   THEN D 0
   THEN Auto
   THEN Unfold `uniform-partition` -1
   THEN (RWO "mklist_length" (-1) THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .  \mforall{}k,m:\mBbbN{}\msupplus{}.    uniform-partition([a,  b];m  *  k)  refines  uniform-partition([a,  b];k\000C)


By

---

Latex:
(Auto
  THEN  (Assert  icompact([a,  b])  BY
                          EAuto  1)
  THEN  D  0
  THEN  Auto
  THEN  Unfold  `uniform-partition`  -1
  THEN  (RWO  "mklist\_length"  (-1)  THENA  Auto))

---

Home Index