---

Step * 2 2 of Lemma partition-split-cons

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

---

Latex:

---

Latex:
.....antecedent..... 
1.  I  :  Interval
2.  icompact(I)
3.  a  :  \mBbbR{}
4.  bs  :  \mBbbR{}  List
5.  frs-non-dec([a  /  bs])
6.  0  <  ||bs||
\mvdash{}  0  <  ||[a  /  bs]||


By

---

Latex:
Auto'

---

Home Index