---

Step * 1 1 1 1 2 1 1 of Lemma nearby-separated-partitions


1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. p : partition(I)@i
5. q : partition(I)@i
6. e : {e:ℝ| r0 < e} @i
7. q1 : partition(I)
8. frs-increasing(q1)
9. ||p|| = ||q1|| ∈ ℤ
10. ∀i:ℕ||p||. (|p[i] - q1[i]| ≤ e)
11. (e/r(2)) ∈ {e:ℝ| r0 < e} 
12. r : partition(I)
13. frs-increasing(r)
14. ||q|| = ||r|| ∈ ℤ
15. ∀i:ℕ||q||. (|q[i] - r[i]| ≤ (e/r(2)))
16. q2 : partition(I)
17. frs-increasing(q2)
18. ||r|| = ||q2|| ∈ ℤ
19. ∀i:ℕ||r||. (|r[i] - q2[i]| ≤ (e/r(2)))
20. i : ℕ||q||@i
⊢ |q[i] - q2[i]| ≤ e
BY
{ ((InstHyp [⌜i⌝] (-6)⋅ THENA Auto) THEN (InstHyp [⌜i⌝] (-3)⋅ THENA Auto)) }

1
1. I : Interval@i
2. icompact(I)
3. iproper(I)
4. p : partition(I)@i
5. q : partition(I)@i
6. e : {e:ℝ| r0 < e} @i
7. q1 : partition(I)
8. frs-increasing(q1)
9. ||p|| = ||q1|| ∈ ℤ
10. ∀i:ℕ||p||. (|p[i] - q1[i]| ≤ e)
11. (e/r(2)) ∈ {e:ℝ| r0 < e} 
12. r : partition(I)
13. frs-increasing(r)
14. ||q|| = ||r|| ∈ ℤ
15. ∀i:ℕ||q||. (|q[i] - r[i]| ≤ (e/r(2)))
16. q2 : partition(I)
17. frs-increasing(q2)
18. ||r|| = ||q2|| ∈ ℤ
19. ∀i:ℕ||r||. (|r[i] - q2[i]| ≤ (e/r(2)))
20. i : ℕ||q||@i
21. |q[i] - r[i]| ≤ (e/r(2))
22. |r[i] - q2[i]| ≤ (e/r(2))
⊢ |q[i] - q2[i]| ≤ e

---

Latex:

---

Latex:

1.  I  :  Interval@i
2.  icompact(I)
3.  iproper(I)
4.  p  :  partition(I)@i
5.  q  :  partition(I)@i
6.  e  :  \{e:\mBbbR{}|  r0  <  e\}  @i
7.  q1  :  partition(I)
8.  frs-increasing(q1)
9.  ||p||  =  ||q1||
10.  \mforall{}i:\mBbbN{}||p||.  (|p[i]  -  q1[i]|  \mleq{}  e)
11.  (e/r(2))  \mmember{}  \{e:\mBbbR{}|  r0  <  e\} 
12.  r  :  partition(I)
13.  frs-increasing(r)
14.  ||q||  =  ||r||
15.  \mforall{}i:\mBbbN{}||q||.  (|q[i]  -  r[i]|  \mleq{}  (e/r(2)))
16.  q2  :  partition(I)
17.  frs-increasing(q2)
18.  ||r||  =  ||q2||
19.  \mforall{}i:\mBbbN{}||r||.  (|r[i]  -  q2[i]|  \mleq{}  (e/r(2)))
20.  i  :  \mBbbN{}||q||@i
\mvdash{}  |q[i]  -  q2[i]|  \mleq{}  e


By

---

Latex:
((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto))

---

Home Index