---

Step * 1 of Lemma partition-sum-bound

.....wf..... 
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. p : partition(I)
6. y : partition-choice(full-partition(I;p))
⊢ y ∈ ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} 
BY
{ (Assert ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ BY
         (Unfold `full-partition` 0 THEN Auto')) }

1
1. I : Interval
2. icompact(I)
3. f : I ⟶ℝ
4. mc : f[x] continuous for x ∈ I
5. p : partition(I)
6. y : partition-choice(full-partition(I;p))
7. ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ
⊢ y ∈ ℕ||p|| + 1 ⟶ {x:ℝ| x ∈ I} 

---

Latex:

---

Latex:
.....wf..... 
1.  I  :  Interval
2.  icompact(I)
3.  f  :  I  {}\mrightarrow{}\mBbbR{}
4.  mc  :  f[x]  continuous  for  x  \mmember{}  I
5.  p  :  partition(I)
6.  y  :  partition-choice(full-partition(I;p))
\mvdash{}  y  \mmember{}  \mBbbN{}||p||  +  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 


By

---

Latex:
(Assert  ||full-partition(I;p)||  =  (||p||  +  2)  BY
              (Unfold  `full-partition`  0  THEN  Auto'))

---

Home Index