---

Step * of Lemma adjacent-full-partition-points

∀[I:Interval]
  ∀[p:partition(I)]
    ∀i:ℕ||full-partition(I;p)|| - 1. r0≤full-partition(I;p)[i + 1] - full-partition(I;p)[i]≤partition-mesh(I;p) 
  supposing icompact(I)
BY
{ (InstLemma `adjacent-partition-points` []
   THEN (ParallelLast' THENA Auto)
   THEN Intros
   THEN (With ⌜%1⌝ (D 2)⋅ THENA Auto)
   THEN (With ⌜p⌝ (D (-1))⋅ THENA Auto)
   THEN Unhide
   THEN Try ((Unfold `rbetween` 0 THEN Complete (Auto)))
   THEN D (-1)
   THEN (Decide ⌜0 < ||p||⌝⋅ THENA Auto)
   THEN ThinTrivial
   THEN Auto
   THEN (Subst' ||full-partition(I;p)|| - 1 ~ ||p|| + 1 4
         THENA (RepUR ``full-partition`` 0 THEN (RWO "length-append" 0 THENA Auto) THEN Reduce 0 THEN Auto)
         )⋅) }

1
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. i : ℕ||p|| + 1
5. (¬0 < ||p||) ⇒ r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;p)
6. 0 < ||p||
7. r0≤p[0] - left-endpoint(I)≤partition-mesh(I;p)
8. ∀i:ℕ||p|| - 1. r0≤p[i + 1] - p[i]≤partition-mesh(I;p)
9. r0≤right-endpoint(I) - last(p)≤partition-mesh(I;p)
⊢ r0≤full-partition(I;p)[i + 1] - full-partition(I;p)[i]≤partition-mesh(I;p)

2
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. i : ℕ||p|| + 1
5. ¬0 < ||p||
6. r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;p)
⊢ r0≤full-partition(I;p)[i + 1] - full-partition(I;p)[i]≤partition-mesh(I;p)

---

Latex:

---

Latex:
\mforall{}[I:Interval]
    \mforall{}[p:partition(I)]
        \mforall{}i:\mBbbN{}||full-partition(I;p)||  -  1
            r0\mleq{}full-partition(I;p)[i  +  1]  -  full-partition(I;p)[i]\mleq{}partition-mesh(I;p) 
    supposing  icompact(I)


By

---

Latex:
(InstLemma  `adjacent-partition-points`  []
  THEN  (ParallelLast'  THENA  Auto)
  THEN  Intros
  THEN  (With  \mkleeneopen{}\%1\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)
  THEN  (With  \mkleeneopen{}p\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  Unhide
  THEN  Try  ((Unfold  `rbetween`  0  THEN  Complete  (Auto)))
  THEN  D  (-1)
  THEN  (Decide  \mkleeneopen{}0  <  ||p||\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinTrivial
  THEN  Auto
  THEN  (Subst'  ||full-partition(I;p)||  -  1  \msim{}  ||p||  +  1  4
              THENA  (RepUR  ``full-partition``  0
                            THEN  (RWO  "length-append"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  Auto)
              )\mcdot{})

---

Home Index