---

Step * 2 of Lemma partition-split-cons


1. I : Interval
2. icompact(I)
3. a : ℝ
4. bs : ℝ List
5. partitions(I;[a / bs])
6. partitions([left-endpoint(I), a];[])
⊢ partitions([a, right-endpoint(I)];bs)
BY
{ (Thin (-1) THEN RepeatFor 3 (ParallelLast)) }

1
1. I : Interval
2. icompact(I)
3. a : ℝ
4. bs : ℝ List
5. 0 < ||[a / bs]|| ⇒ ((left-endpoint(I) ≤ [a / bs][0]) ∧ (last([a / bs]) ≤ right-endpoint(I)))
6. ∀i,j:ℕ||[a / bs]||.  ((i ≤ j) ⇒ ([a / bs][i] ≤ [a / bs][j]))
⊢ ∀i,j:ℕ||bs||.  ((i ≤ j) ⇒ (bs[i] ≤ bs[j]))

2
.....antecedent..... 
1. I : Interval
2. icompact(I)
3. a : ℝ
4. bs : ℝ List
5. frs-non-dec([a / bs])
6. 0 < ||bs||
⊢ 0 < ||[a / bs]||

3
1. I : Interval
2. icompact(I)
3. a : ℝ
4. bs : ℝ List
5. frs-non-dec([a / bs])
6. 0 < ||bs||
7. (left-endpoint(I) ≤ [a / bs][0]) ∧ (last([a / bs]) ≤ right-endpoint(I))
⊢ (left-endpoint([a, right-endpoint(I)]) ≤ bs[0]) ∧ (last(bs) ≤ right-endpoint([a, right-endpoint(I)]))

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  a  :  \mBbbR{}
4.  bs  :  \mBbbR{}  List
5.  partitions(I;[a  /  bs])
6.  partitions([left-endpoint(I),  a];[])
\mvdash{}  partitions([a,  right-endpoint(I)];bs)


By

---

Latex:
(Thin  (-1)  THEN  RepeatFor  3  (ParallelLast))

---

Home Index