---

Step * 1 1 1 1 1 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. nearby-partitions(e;p;q1)
10. (e/r(2)) ∈ {e:ℝ| r0 < e} 
11. r : partition(I)
12. frs-increasing(r)
13. nearby-partitions((e/r(2));q;r)
14. q2 : partition(I)
15. frs-increasing(q2)
16. nearby-partitions((e/r(2));r;q2)
17. (∀x∈q2.(∀y∈q1.x ≠ y))
18. frs-increasing(q2)
⊢ (∀x∈q1.(∀y∈q2.x ≠ y))
BY
{ ((RWW "l_all_iff" (-2) THENA Auto) THEN (RWW "l_all_iff" 0 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. nearby-partitions(e;p;q1)
10. (e/r(2)) ∈ {e:ℝ| r0 < e} 
11. r : partition(I)
12. frs-increasing(r)
13. nearby-partitions((e/r(2));q;r)
14. q2 : partition(I)
15. frs-increasing(q2)
16. nearby-partitions((e/r(2));r;q2)
17. ∀x:ℝ. ((x ∈ q2) ⇒ (∀y:ℝ. ((y ∈ q1) ⇒ x ≠ y)))
18. frs-increasing(q2)
⊢ ∀x:ℝ. ((x ∈ q1) ⇒ (∀y:ℝ. ((y ∈ q2) ⇒ x ≠ y)))

---

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.  nearby-partitions(e;p;q1)
10.  (e/r(2))  \mmember{}  \{e:\mBbbR{}|  r0  <  e\} 
11.  r  :  partition(I)
12.  frs-increasing(r)
13.  nearby-partitions((e/r(2));q;r)
14.  q2  :  partition(I)
15.  frs-increasing(q2)
16.  nearby-partitions((e/r(2));r;q2)
17.  (\mforall{}x\mmember{}q2.(\mforall{}y\mmember{}q1.x  \mneq{}  y))
18.  frs-increasing(q2)
\mvdash{}  (\mforall{}x\mmember{}q1.(\mforall{}y\mmember{}q2.x  \mneq{}  y))


By

---

Latex:
((RWW  "l\_all\_iff"  (-2)  THENA  Auto)  THEN  (RWW  "l\_all\_iff"  0  THENA  Auto))

---

Home Index