---

Step * 1 1 2 1 of Lemma mesh-property


1. I : Interval
2. icompact(I)
3. [%22] : partitions(I;[])
4. e : ℝ
5. r0 < e
6. partition-mesh(I;[]) ≤ e
7. x : ℝ
8. x ∈ I
9. full-partition(I;[])[0]≤x≤full-partition(I;[])[||full-partition(I;[])|| - 1]
10. ||full-partition(I;[])|| = 2 ∈ ℤ
11. i : ℕ1
12. ¬0 < 0
13. r0≤right-endpoint(I) - left-endpoint(I)≤partition-mesh(I;[])
⊢ r0≤full-partition(I;[])[i + 1] - full-partition(I;[])[i]≤partition-mesh(I;[])
BY
{ (Subst ⌜i ~ 0⌝ 0⋅ THEN Auto' THEN RepUR ``full-partition`` 0) }

---

Latex:

---

Latex:

1.  I  :  Interval
2.  icompact(I)
3.  [\%22]  :  partitions(I;[])
4.  e  :  \mBbbR{}
5.  r0  <  e
6.  partition-mesh(I;[])  \mleq{}  e
7.  x  :  \mBbbR{}
8.  x  \mmember{}  I
9.  full-partition(I;[])[0]\mleq{}x\mleq{}full-partition(I;[])[||full-partition(I;[])||  -  1]
10.  ||full-partition(I;[])||  =  2
11.  i  :  \mBbbN{}1
12.  \mneg{}0  <  0
13.  r0\mleq{}right-endpoint(I)  -  left-endpoint(I)\mleq{}partition-mesh(I;[])
\mvdash{}  r0\mleq{}full-partition(I;[])[i  +  1]  -  full-partition(I;[])[i]\mleq{}partition-mesh(I;[])


By

---

Latex:
(Subst  \mkleeneopen{}i  \msim{}  0\mkleeneclose{}  0\mcdot{}  THEN  Auto'  THEN  RepUR  ``full-partition``  0)

---

Home Index