---

Step * 1 2 1 of Lemma simple-partition-exists


1. a : ℝ
2. b : ℝ
3. a ≤ b
4. e : ℝ
5. r0 < e
6. icompact([a, b])
7. p : partition([a, b])
8. partition-mesh([a, b];p) ≤ e
9. ∀i:ℕ||full-partition([a, b];p)||. (full-partition([a, b];p)[i] ∈ [a, b])
10. full-partition([a, b];p)[0] = a ∈ ℝ
⊢ full-partition([a, b];p)[||full-partition([a, b];p)|| - 1] = b ∈ ℝ
BY
{ (RepUR ``full-partition left-endpoint right-endpoint endpoints`` 0 THEN Auto) }

1
1. a : ℝ
2. b : ℝ
3. a ≤ b
4. e : ℝ
5. r0 < e
6. icompact([a, b])
7. p : partition([a, b])
8. partition-mesh([a, b];p) ≤ e
9. ∀i:ℕ||full-partition([a, b];p)||. (full-partition([a, b];p)[i] ∈ [a, b])
10. full-partition([a, b];p)[0] = a ∈ ℝ
⊢ [a / (p @ [b])][((||p|| + 1) + 1) - 1] = b ∈ ℝ

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  \mleq{}  b
4.  e  :  \mBbbR{}
5.  r0  <  e
6.  icompact([a,  b])
7.  p  :  partition([a,  b])
8.  partition-mesh([a,  b];p)  \mleq{}  e
9.  \mforall{}i:\mBbbN{}||full-partition([a,  b];p)||.  (full-partition([a,  b];p)[i]  \mmember{}  [a,  b])
10.  full-partition([a,  b];p)[0]  =  a
\mvdash{}  full-partition([a,  b];p)[||full-partition([a,  b];p)||  -  1]  =  b


By

---

Latex:
(RepUR  ``full-partition  left-endpoint  right-endpoint  endpoints``  0  THEN  Auto)

---

Home Index