Step
*
2
of Lemma
adjacent-full-partition-points
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)
BY
{ (CaseNat 0 `i' THEN Auto') }
1
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)
7. i = 0 ∈ ℤ
⊢ r0≤full-partition(I;p)[0 + 1] - full-partition(I;p)[0]≤partition-mesh(I;p)
Latex:
Latex:
1. I : Interval
2. icompact(I)
3. p : partition(I)
4. i : \mBbbN{}||p|| + 1
5. \mneg{}0 < ||p||
6. r0\mleq{}right-endpoint(I) - left-endpoint(I)\mleq{}partition-mesh(I;p)
\mvdash{} r0\mleq{}full-partition(I;p)[i + 1] - full-partition(I;p)[i]\mleq{}partition-mesh(I;p)
By
Latex:
(CaseNat 0 `i' THEN Auto')
Home
Index