---

Step * of Lemma nearby-separated-partition-sum

∀I:Interval
  (icompact(I)
  ⇒ iproper(I)
  ⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀alpha,e:{e:ℝ| r0 < e} . ∀p,q:partition(I).
      ∀x:partition-choice(full-partition(I;p)). ∀y:partition-choice(full-partition(I;q)).
        ∃p':partition(I)
         ∃x':partition-choice(full-partition(I;p'))
          ((partition-mesh(I;p') ≤ (partition-mesh(I;p) + e))
          ∧ (∃q':partition(I)
              ∃y':partition-choice(full-partition(I;q'))
               (separated-partitions(p';q')
               ∧ (partition-mesh(I;q') ≤ (partition-mesh(I;q) + e))
               ∧ (|S(f;full-partition(I;p)) - S(f;full-partition(I;q))| ≤ (|S(f;full-partition(I;p')) 
                 - S(f;full-partition(I;q'))|
                 + alpha)))))))
BY
{ TACTIC:(Auto
          THEN ((Assert r0 < (alpha/r(2)) BY
                       (nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
                THEN (Assert r0 < (e/r(2)) BY
                            (nRMul ⌜r(2)⌝ 0⋅ THEN Auto))
                )
          THEN (InstLemma `nearby-partition-sum` [⌜I⌝;⌜f⌝;⌜mc⌝;⌜p⌝;⌜x⌝;⌜(alpha/r(2))⌝]⋅ THENA Auto)
          THEN ExRepD
          THEN (InstLemma `nearby-partition-sum` [⌜I⌝;⌜f⌝;⌜mc⌝;⌜q⌝;⌜y⌝;⌜(alpha/r(2))⌝]⋅ THENA Auto)
          THEN ExRepD) }

1
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. f : I ⟶ℝ@i
5. mc : f[x] continuous for x ∈ I@i
6. alpha : {alpha:ℝ| r0 < alpha} @i
7. e : {e:ℝ| r0 < e} @i
8. p : partition(I)@i
9. q : partition(I)@i
10. x : partition-choice(full-partition(I;p))@i
11. y : partition-choice(full-partition(I;q))@i
12. r0 < (alpha/r(2))
13. r0 < (e/r(2))
14. e1 : {e:ℝ| r0 < e} 
15. ∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
      (nearby-partitions(e1;p;q)
      ⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e1))
      ⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (alpha/r(2))))
16. e2 : {e:ℝ| r0 < e} 
17. ∀q@0:partition(I). ∀y@0:partition-choice(full-partition(I;q@0)).
      (nearby-partitions(e2;q;q@0)
      ⇒ (∀i:ℕ||q|| + 1. (|y[i] - y@0[i]| ≤ e2))
      ⇒ (|S(f;full-partition(I;q@0)) - S(f;full-partition(I;q))| ≤ (alpha/r(2))))
⊢ ∃p':partition(I)
   ∃x':partition-choice(full-partition(I;p'))
    ((partition-mesh(I;p') ≤ (partition-mesh(I;p) + e))
    ∧ (∃q':partition(I)
        ∃y':partition-choice(full-partition(I;q'))
         (separated-partitions(p';q')
         ∧ (partition-mesh(I;q') ≤ (partition-mesh(I;q) + e))
         ∧ (|S(f;full-partition(I;p)) - S(f;full-partition(I;q))| ≤ (|S(f;full-partition(I;p')) 
           - S(f;full-partition(I;q'))|
           + alpha)))))

---

Latex:

---

Latex:
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  iproper(I)
    {}\mRightarrow{}  (\mforall{}f:I  {}\mrightarrow{}\mBbbR{}.  \mforall{}mc:f[x]  continuous  for  x  \mmember{}  I.  \mforall{}alpha,e:\{e:\mBbbR{}|  r0  <  e\}  .  \mforall{}p,q:partition(I).
            \mforall{}x:partition-choice(full-partition(I;p)).  \mforall{}y:partition-choice(full-partition(I;q)).
                \mexists{}p':partition(I)
                  \mexists{}x':partition-choice(full-partition(I;p'))
                    ((partition-mesh(I;p')  \mleq{}  (partition-mesh(I;p)  +  e))
                    \mwedge{}  (\mexists{}q':partition(I)
                            \mexists{}y':partition-choice(full-partition(I;q'))
                              (separated-partitions(p';q')
                              \mwedge{}  (partition-mesh(I;q')  \mleq{}  (partition-mesh(I;q)  +  e))
                              \mwedge{}  (|S(f;full-partition(I;p)) 
                                  -  S(f;full-partition(I;q))|  \mleq{}  (|S(f;full-partition(I;p')) 
                                  -  S(f;full-partition(I;q'))|
                                  +  alpha)))))))


By

---

Latex:
TACTIC:(Auto
                THEN  ((Assert  r0  <  (alpha/r(2))  BY
                                          (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
                            THEN  (Assert  r0  <  (e/r(2))  BY
                                                    (nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}  THEN  Auto))
                            )
                THEN  (InstLemma  `nearby-partition-sum`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}(alpha/r(2))\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ExRepD
                THEN  (InstLemma  `nearby-partition-sum`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}mc\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}(alpha/r(2))\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ExRepD)

---

Home Index