---

Step * of Lemma adjacent-partition-points

No Annotations
∀[I:Interval]
  ∀[p:partition(I)]
    (((¬0 < ||p||) ⇒ r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;p))
    ∧ (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)))) 
  supposing icompact(I)
BY
{ (RepeatFor 3 ((D 0 THENA (Auto THEN DVar `p' THEN Auto)))
   THEN ((InstLemma `adjacent-frs-points` [⌜full-partition(I;p)⌝]⋅ THENA Auto)
         THEN Fold `partition-mesh` (-1)
         THEN (InstLemma `full-partition-non-dec` [⌜I⌝;⌜p⌝]⋅ THENA Auto)
         THEN (Assert ∀i:ℕ||p|| + 1. r0≤full-partition(I;p)[i + 1] - full-partition(I;p)[i]≤partition-mesh(I;p) BY
                     (((D 0 THENA Auto) THEN (BHyp -3 THENA (RepUR ``full-partition`` 0 THEN Auto'))) THEN Auto)))⋅
   ) }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. ∀[i:ℕ||full-partition(I;p)|| - 1]
     (frs-non-dec(full-partition(I;p)) ⇒ r0≤full-partition(I;p)[i + 1] - full-partition(I;p)[i]≤partition-mesh(I;p))
5. frs-non-dec(full-partition(I;p))
6. ∀i:ℕ||p|| + 1. r0≤full-partition(I;p)[i + 1] - full-partition(I;p)[i]≤partition-mesh(I;p)
⊢ ((¬0 < ||p||) ⇒ r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;p))
∧ (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)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[I:Interval]
    \mforall{}[p:partition(I)]
        (((\mneg{}0  <  ||p||)  {}\mRightarrow{}  r0\mleq{}right-endpoint(I)  -  left-endpoint(I)\mleq{}partition-mesh(I;p))
        \mwedge{}  (0  <  ||p||
            {}\mRightarrow{}  (r0\mleq{}p[0]  -  left-endpoint(I)\mleq{}partition-mesh(I;p)
                  \mwedge{}  (\mforall{}i:\mBbbN{}||p||  -  1.  r0\mleq{}p[i  +  1]  -  p[i]\mleq{}partition-mesh(I;p))
                  \mwedge{}  r0\mleq{}right-endpoint(I)  -  last(p)\mleq{}partition-mesh(I;p)))) 
    supposing  icompact(I)


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  (Auto  THEN  DVar  `p'  THEN  Auto)))
  THEN  ((InstLemma  `adjacent-frs-points`  [\mkleeneopen{}full-partition(I;p)\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  Fold  `partition-mesh`  (-1)
              THEN  (InstLemma  `full-partition-non-dec`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (Assert  \mforall{}i:\mBbbN{}||p||  +  1
                                            r0\mleq{}full-partition(I;p)[i  +  1]  -  full-partition(I;p)[i]\mleq{}partition-mesh(I;p)  BY
                                      (((D  0  THENA  Auto)  THEN  (BHyp  -3  THENA  (RepUR  ``full-partition``  0  THEN  Auto')))
                                        THEN  Auto
                                        )))\mcdot{}
  )

---

Home Index