Step
*
1
2
1
2
1
1
of Lemma
adjacent-full-partition-points
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. i : ℕ||p|| + 1
5. ¬(i + 1) - 1 < ||p||
6. (¬0 < ||p||)
⇒ r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;p)
7. 0 < ||p||
8. r0≤p[0] - left-endpoint(I)≤partition-mesh(I;p)
9. ∀i:ℕ||p|| - 1. r0≤p[i + 1] - p[i]≤partition-mesh(I;p)
10. r0≤right-endpoint(I) - last(p)≤partition-mesh(I;p)
11. ¬(i = 0 ∈ ℤ)
12. ¬i < ||p||
⊢ [right-endpoint(I)][(i + 1) - 1 - ||p||] ~ right-endpoint(I)
BY
{ (Subst ⌜(i + 1) - 1 - ||p|| ~ 0⌝ 0⋅ THEN Reduce 0 THEN Auto) }
Latex:
Latex:
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. i : \mBbbN{}||p|| + 1
5. \mneg{}(i + 1) - 1 < ||p||
6. (\mneg{}0 < ||p||) {}\mRightarrow{} r0\mleq{}right-endpoint(I) - left-endpoint(I)\mleq{}partition-mesh(I;p)
7. 0 < ||p||
8. r0\mleq{}p[0] - left-endpoint(I)\mleq{}partition-mesh(I;p)
9. \mforall{}i:\mBbbN{}||p|| - 1. r0\mleq{}p[i + 1] - p[i]\mleq{}partition-mesh(I;p)
10. r0\mleq{}right-endpoint(I) - last(p)\mleq{}partition-mesh(I;p)
11. \mneg{}(i = 0)
12. \mneg{}i < ||p||
\mvdash{} [right-endpoint(I)][(i + 1) - 1 - ||p||] \msim{} right-endpoint(I)
By
Latex:
(Subst \mkleeneopen{}(i + 1) - 1 - ||p|| \msim{} 0\mkleeneclose{} 0\mcdot{} THEN Reduce 0 THEN Auto)
Home
Index