---

Step * 1 1 of Lemma partition-sum-bound


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} 
BY
{ ((FunExt THENA Auto)
   THEN DoSubsume
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN (InstLemma `full-partition-point-member` [⌜I⌝;⌜p⌝]⋅ THENA Auto)
   THEN DupHyp (-1)
   THEN (D -1 With ⌜x⌝  THENA Auto)
   THEN MoveToConcl (-1)
   THEN (D -1 With ⌜x + 1⌝  THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜full-partition(I;p)[x]⌝;⌜full-partition(I;p)[x + 1]⌝]⋅
   THEN All Thin
   THEN Auto
   THEN (InstLemma `i-member-between` [⌜I⌝;⌜v⌝;⌜v1⌝]⋅ THENA Auto)
   THEN BHyp -1
   THEN Auto) }

---

Latex:

---

Latex:

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))
7.  ||full-partition(I;p)||  =  (||p||  +  2)
\mvdash{}  y  \mmember{}  \mBbbN{}||p||  +  1  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  I\} 


By

---

Latex:
((FunExt  THENA  Auto)
  THEN  DoSubsume
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (InstLemma  `full-partition-point-member`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  (D  -1  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (D  -1  With  \mkleeneopen{}x  +  1\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}full-partition(I;p)[x]\mkleeneclose{};\mkleeneopen{}full-partition(I;p)[x  +  1]\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto
  THEN  (InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1
  THEN  Auto)

---

Home Index