Step
*
1
1
1
2
2
1
1
of Lemma
real-subset-connected-lemma
1. X : ℝ ⟶ ℙ
2. dense-in-interval((-∞, ∞);X)
3. a : {x:ℝ| X x} ⟶ 𝔹
4. b : {x:ℝ| X x} ⟶ 𝔹
5. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
6. a0 : {x:ℝ| X x}
7. b0 : {x:ℝ| X x}
8. ↑(a a0)
9. ↑(b b0)
10. a0 < b0
11. ∀u,v:{x:ℝ| X x} .
((u < v)
⇒ (∃p:{x:ℝ| X x}
(((u < p) ∧ (p < v)) ∧ ((p - u) ≤ ((r(2)/r(3)) * (v - u))) ∧ ((v - p) ≤ ((r(2)/r(3)) * (v - u))))))
12. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
∃pq':{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd(pq')) - fst(pq')) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
((pq' = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ (pq' = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )))))
13. h : pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} ⟶ {pq:{x:ℝ| X\000C x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq)))
∧ (↑(a (fst(pq))))
∧ (↑(b (snd(pq))))}
14. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd((h pq))) - fst((h pq))) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
(((h pq) = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ ((h pq) = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} \000C)))))
15. ∀n:ℕ
(primrec(n;<a0, b0>;λi.h) ∈ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} )
⊢ ∃h:ℕ ⟶ ({x:ℝ| X x} × {x:ℝ| X x} )
(((fst(h[0])) < (snd(h[0])))
∧ (∀n:ℕ
((↑(a (fst(h[n]))))
∧ (↑(b (snd(h[n]))))
∧ let a,b = h[n]
in ∃p:{x:ℝ| X x}
(((a < p) ∧ (p < b))
∧ (((h[n + 1] = <a, p> ∈ (ℝ × ℝ)) ∧ ((p - a) ≤ ((r(2)/r(3)) * (b - a))))
∨ ((h[n + 1] = <p, b> ∈ (ℝ × ℝ)) ∧ ((b - p) ≤ ((r(2)/r(3)) * (b - a)))))))))
BY
{ (Assert λn.primrec(n;<a0, b0>;λi.h) ∈ ℕ ⟶ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} BY
Auto) }
1
1. X : ℝ ⟶ ℙ
2. dense-in-interval((-∞, ∞);X)
3. a : {x:ℝ| X x} ⟶ 𝔹
4. b : {x:ℝ| X x} ⟶ 𝔹
5. ∀x:{x:ℝ| X x} . ((↑(a x)) ∨ (↑(b x)))
6. a0 : {x:ℝ| X x}
7. b0 : {x:ℝ| X x}
8. ↑(a a0)
9. ↑(b b0)
10. a0 < b0
11. ∀u,v:{x:ℝ| X x} .
((u < v)
⇒ (∃p:{x:ℝ| X x}
(((u < p) ∧ (p < v)) ∧ ((p - u) ≤ ((r(2)/r(3)) * (v - u))) ∧ ((v - p) ≤ ((r(2)/r(3)) * (v - u))))))
12. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
∃pq':{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd(pq')) - fst(pq')) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
((pq' = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ (pq' = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )))))
13. h : pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} ⟶ {pq:{x:ℝ| X\000C x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq)))
∧ (↑(a (fst(pq))))
∧ (↑(b (snd(pq))))}
14. ∀pq:{pq:{x:ℝ| X x} × {x:ℝ| X x} | ((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
((((snd((h pq))) - fst((h pq))) ≤ ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
∧ (∃xx:{x:ℝ| X x}
(((h pq) = <fst(pq), xx> ∈ ({x:ℝ| X x} × {x:ℝ| X x} )) ∨ ((h pq) = <xx, snd(pq)> ∈ ({x:ℝ| X x} × {x:ℝ| X x} \000C)))))
15. ∀n:ℕ
(primrec(n;<a0, b0>;λi.h) ∈ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))} )
16. λn.primrec(n;<a0, b0>;λi.h) ∈ ℕ ⟶ {pq:{x:ℝ| X x} × {x:ℝ| X x} |
((fst(pq)) < (snd(pq))) ∧ (↑(a (fst(pq)))) ∧ (↑(b (snd(pq))))}
⊢ ∃h:ℕ ⟶ ({x:ℝ| X x} × {x:ℝ| X x} )
(((fst(h[0])) < (snd(h[0])))
∧ (∀n:ℕ
((↑(a (fst(h[n]))))
∧ (↑(b (snd(h[n]))))
∧ let a,b = h[n]
in ∃p:{x:ℝ| X x}
(((a < p) ∧ (p < b))
∧ (((h[n + 1] = <a, p> ∈ (ℝ × ℝ)) ∧ ((p - a) ≤ ((r(2)/r(3)) * (b - a))))
∨ ((h[n + 1] = <p, b> ∈ (ℝ × ℝ)) ∧ ((b - p) ≤ ((r(2)/r(3)) * (b - a)))))))))
Latex:
Latex:
1. X : \mBbbR{} {}\mrightarrow{} \mBbbP{}
2. dense-in-interval((-\minfty{}, \minfty{});X)
3. a : \{x:\mBbbR{}| X x\} {}\mrightarrow{} \mBbbB{}
4. b : \{x:\mBbbR{}| X x\} {}\mrightarrow{} \mBbbB{}
5. \mforall{}x:\{x:\mBbbR{}| X x\} . ((\muparrow{}(a x)) \mvee{} (\muparrow{}(b x)))
6. a0 : \{x:\mBbbR{}| X x\}
7. b0 : \{x:\mBbbR{}| X x\}
8. \muparrow{}(a a0)
9. \muparrow{}(b b0)
10. a0 < b0
11. \mforall{}u,v:\{x:\mBbbR{}| X x\} .
((u < v)
{}\mRightarrow{} (\mexists{}p:\{x:\mBbbR{}| X x\}
(((u < p) \mwedge{} (p < v))
\mwedge{} ((p - u) \mleq{} ((r(2)/r(3)) * (v - u)))
\mwedge{} ((v - p) \mleq{} ((r(2)/r(3)) * (v - u))))))
12. \mforall{}pq:\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\000C\}
\mexists{}pq':\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq)\000C)))\}
((((snd(pq')) - fst(pq')) \mleq{} ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
\mwedge{} (\mexists{}xx:\{x:\mBbbR{}| X x\} . ((pq' = <fst(pq), xx>) \mvee{} (pq' = <xx, snd(pq)>))))
13. h : pq:\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq)\000C)))\}
{}\mrightarrow{} \{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\}
14. \mforall{}pq:\{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} | ((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\000C\}
((((snd((h pq))) - fst((h pq))) \mleq{} ((r(2)/r(3)) * ((snd(pq)) - fst(pq))))
\mwedge{} (\mexists{}xx:\{x:\mBbbR{}| X x\} . (((h pq) = <fst(pq), xx>) \mvee{} ((h pq) = <xx, snd(pq)>))))
15. \mforall{}n:\mBbbN{}
(primrec(n;<a0, b0>\mlambda{}i.h) \mmember{} \{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} |
((fst(pq)) < (snd(pq))) \mwedge{} (\muparrow{}(a (fst(pq)))) \mwedge{} (\muparrow{}(b (snd(pq))))\} )
\mvdash{} \mexists{}h:\mBbbN{} {}\mrightarrow{} (\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} )
(((fst(h[0])) < (snd(h[0])))
\mwedge{} (\mforall{}n:\mBbbN{}
((\muparrow{}(a (fst(h[n]))))
\mwedge{} (\muparrow{}(b (snd(h[n]))))
\mwedge{} let a,b = h[n]
in \mexists{}p:\{x:\mBbbR{}| X x\}
(((a < p) \mwedge{} (p < b))
\mwedge{} (((h[n + 1] = <a, p>) \mwedge{} ((p - a) \mleq{} ((r(2)/r(3)) * (b - a))))
\mvee{} ((h[n + 1] = <p, b>) \mwedge{} ((b - p) \mleq{} ((r(2)/r(3)) * (b - a)))))))))
By
Latex:
(Assert \mlambda{}n.primrec(n;<a0, b0>\mlambda{}i.h) \mmember{} \mBbbN{} {}\mrightarrow{} \{pq:\{x:\mBbbR{}| X x\} \mtimes{} \{x:\mBbbR{}| X x\} |
((fst(pq)) < (snd(pq)))
\mwedge{} (\muparrow{}(a (fst(pq))))
\mwedge{} (\muparrow{}(b (snd(pq))))\} BY
Auto)
Home
Index