Step
*
1
of Lemma
uniform-partition-increasing
1. a : ℝ
2. b : ℝ
3. a < b
4. k : ℕ+
5. icompact([a, b])
⊢ frs-increasing(uniform-partition([a, b];k))
BY
{ (D 0
THEN Auto
THEN All (RepUR ``uniform-partition``)
THEN All (RWO "mklist_length mklist_select")
THEN Auto
THEN Reduce 0) }
1
1. a : ℝ
2. b : ℝ
3. a < b
4. k : ℕ+
5. icompact([a, b])
6. i : ℕk - 1
7. j : ℕk - 1
8. i < j
⊢ (((r(k) - r(i + 1)) * a) + (r(i + 1) * b)/r(k)) < (((r(k) - r(j + 1)) * a) + (r(j + 1) * b)/r(k))
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. a < b
4. k : \mBbbN{}\msupplus{}
5. icompact([a, b])
\mvdash{} frs-increasing(uniform-partition([a, b];k))
By
Latex:
(D 0
THEN Auto
THEN All (RepUR ``uniform-partition``)
THEN All (RWO "mklist\_length mklist\_select")
THEN Auto
THEN Reduce 0)
Home
Index