---

Step * 1 2 1 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 ∈ ℝ
⊢ [a / (p @ [b])][((||p|| + 1) + 1) - 1] = b ∈ ℝ
BY
{ ((RWO "select_cons_tl" 0 THEN Auto) THEN RWO "select_append_back" 0 THEN Auto) }

---

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{}  [a  /  (p  @  [b])][((||p||  +  1)  +  1)  -  1]  =  b


By

---

Latex:
((RWO  "select\_cons\_tl"  0  THEN  Auto)  THEN  RWO  "select\_append\_back"  0  THEN  Auto)

---

Home Index