[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
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` THEN Complete (Auto)))
THEN (-1)
THEN (Decide ⌜0 < ||p||⌝⋅ THENA Auto)
THEN ThinTrivial
THEN Auto
THEN (Subst' ||full-partition(I;p)|| ||p|| 4
THENA (RepUR ``full-partition`` THEN (RWO "length-append" THENA Auto) THEN Reduce THEN Auto)
)⋅}

1
1. Interval
2. icompact(I)
3. partition(I)
4. : ℕ||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. Interval
2. icompact(I)
3. partition(I)
4. : ℕ||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:
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