---

Step * of Lemma mesh-property

No Annotations
∀I:Interval
  (icompact(I)
  ⇒ (∀p:partition(I). ∀e:ℝ.
        ((r0 < e)
        ⇒ ∀x:ℝ. ((x ∈ I) ⇒ (∃i:ℕ||full-partition(I;p)||. (|x - full-partition(I;p)[i]| ≤ e))) 
           supposing partition-mesh(I;p) ≤ e)))
BY
{ (Auto
   THEN ((InstLemma `partition-endpoints` [⌜I⌝; ⌜p⌝; ⌜x⌝])⋅ THENA Auto)
   THEN ((InstLemma `adjacent-partition-points` [⌜I⌝; ⌜p⌝])⋅ THENA Auto)⋅
   THEN (Assert ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ BY
               (RepUR ``full-partition`` 0 THEN Auto'))
   THEN ((InstLemma `partition-lemma` [⌜e⌝; ⌜||p|| + 2⌝; ⌜λi.full-partition(I;p)[i]⌝; ⌜x⌝])⋅
         THEN Auto
         THEN All Reduce
         THEN Try ((HypSubst' (-2) 0 THEN Auto)))⋅) }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. e : ℝ
5. r0 < e
6. partition-mesh(I;p) ≤ e
7. x : ℝ
8. x ∈ I
9. full-partition(I;p)[0]≤x≤full-partition(I;p)[||full-partition(I;p)|| - 1]
10. (¬0 < ||p||) ⇒ r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;p)
11. 0 < ||p||
⇒ (r0≤p[0] - left-endpoint(I)≤partition-mesh(I;p)
   ∧ (∀i:ℕ||p|| - 1. r0≤p[i + 1] - p[i]≤partition-mesh(I;p))
   ∧ r0≤right-endpoint(I) - last(p)≤partition-mesh(I;p))
12. ||full-partition(I;p)|| = (||p|| + 2) ∈ ℤ
13. i : ℕ(||p|| + 2) - 1
⊢ r0≤full-partition(I;p)[i + 1] - full-partition(I;p)[i]≤e

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval
    (icompact(I)
    {}\mRightarrow{}  (\mforall{}p:partition(I).  \mforall{}e:\mBbbR{}.
                ((r0  <  e)
                {}\mRightarrow{}  \mforall{}x:\mBbbR{}.  ((x  \mmember{}  I)  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||full-partition(I;p)||.  (|x  -  full-partition(I;p)[i]|  \mleq{}  e))) 
                      supposing  partition-mesh(I;p)  \mleq{}  e)))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `partition-endpoints`  [\mkleeneopen{}I\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `adjacent-partition-points`  [\mkleeneopen{}I\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{}])\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (Assert  ||full-partition(I;p)||  =  (||p||  +  2)  BY
                          (RepUR  ``full-partition``  0  THEN  Auto'))
  THEN  ((InstLemma  `partition-lemma`  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}||p||  +  2\mkleeneclose{};  \mkleeneopen{}\mlambda{}i.full-partition(I;p)[i]\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}])\mcdot{}
              THEN  Auto
              THEN  All  Reduce
              THEN  Try  ((HypSubst'  (-2)  0  THEN  Auto)))\mcdot{})

---

Home Index