Step
*
of Lemma
inhabited-covers-real-implies-ext
∀[A,B:ℝ ⟶ ℙ].
((∃a:ℝ. A[a])
⇒ (∃b:ℝ. B[b])
⇒ (∀r:ℝ. (A[r] ∨ B[r]))
⇒ (∃f,g:ℕ ⟶ ℝ. ∃x:ℝ. ((∀n:ℕ. A[f n]) ∧ (∀n:ℕ. B[g n]) ∧ lim n→∞.f n = x ∧ lim n→∞.g n = x)))
BY
{ Extract of Obid: inhabited-covers-real-implies
not unfolding log imax cover-seq accelerate realops absval rabs canonical-bound pi1 pi2 primrec
finishing with ((RWO "cover-seq-0" 0 THENA Auto) THEN RepUR ``let cover-real`` 0 THEN Auto)
normalizes to:
λ%,%1,%2. let b,%2@0 = %1
in let a,%3 = %
in eval x = canonical-bound(|(fst(<a, b>)) - snd(<a, b>)|) in
<λn.(fst(cover-seq(%2;a;b;n)))
, λn.(snd(cover-seq(%2;a;b;n)))
, accelerate(2;λn@0.((fst(cover-seq(%2;a;b;log(2;n@0 * (x + 1))))) n@0))
, λn.(fst(primrec(n;if %2 (a + b/r(2)) then <%3, %2@0, inr Ax > else <%3, %2@0, inl Ax> fi ;
λi,x. let A,B,_ = x in
<let v1,v2 = cover-seq(%2;a;b;(i + 1) - 1)
in case %2 (v1 + v2/r(2)) of inl(x) => x | inr(y) => A
, let v1,v2 = cover-seq(%2;a;b;(i + 1) - 1)
in case %2 (v1 + v2/r(2)) of inl(x) => B | inr(y) => y
, let v1,v2 = cover-seq(%2;a;b;i + 1)
in if %2 (v1 + v2/r(2)) then inr Ax else inl Ax fi >)))
, λn.let %11,%13,%14 = primrec(n;if %2 (a + b/r(2))
then <%3, %2@0, inr Ax >
else <%3, %2@0, inl Ax>
fi ;λi,x. let A,B,_ = x in
<let v1,v2 = cover-seq(%2;a;b;(i + 1) - 1)
in case %2 (v1 + v2/r(2)) of inl(x) => x | inr(y) => A
, let v1,v2 = cover-seq(%2;a;b;(i + 1) - 1)
in case %2 (v1 + v2/r(2)) of inl(x) => B | inr(y) => y
, let v1,v2 = cover-seq(%2;a;b;i + 1)
in if %2 (v1 + v2/r(2)) then inr Ax else inl Ax fi >) in
%13
, λk.(log(2;(4 * k) * (x + 1)) + 1)
, λk.imax(log(2;(4 * 2 * k) * (x + 1)) + 1;log(2;(2 * k) * (x + 1)))> }
Latex:
Latex:
\mforall{}[A,B:\mBbbR{} {}\mrightarrow{} \mBbbP{}].
((\mexists{}a:\mBbbR{}. A[a])
{}\mRightarrow{} (\mexists{}b:\mBbbR{}. B[b])
{}\mRightarrow{} (\mforall{}r:\mBbbR{}. (A[r] \mvee{} B[r]))
{}\mRightarrow{} (\mexists{}f,g:\mBbbN{} {}\mrightarrow{} \mBbbR{}. \mexists{}x:\mBbbR{}. ((\mforall{}n:\mBbbN{}. A[f n]) \mwedge{} (\mforall{}n:\mBbbN{}. B[g n]) \mwedge{} lim n\mrightarrow{}\minfty{}.f n = x \mwedge{} lim n\mrightarrow{}\minfty{}.g n = x)))
By
Latex:
Extract of Obid: inhabited-covers-real-implies
not unfolding log imax cover-seq accelerate realops absval rabs canonical-bound pi1 pi2 primrec
finishing with ((RWO "cover-seq-0" 0 THENA Auto) THEN RepUR ``let cover-real`` 0 THEN Auto)
normalizes to:
\mlambda{}\%,\%1,\%2. let b,\%2@0 = \%1
in let a,\%3 = \%
in eval x = canonical-bound(|(fst(<a, b>)) - snd(<a, b>)|) in
<\mlambda{}n.(fst(cover-seq(\%2;a;b;n)))
, \mlambda{}n.(snd(cover-seq(\%2;a;b;n)))
, accelerate(2;\mlambda{}n@0.((fst(cover-seq(\%2;a;b;log(2;n@0 * (x + 1))))) n@0))
, \mlambda{}n.(fst(primrec(n;if \%2 (a + b/r(2))
then <\%3, \%2@0, inr Ax >
else <\%3, \%2@0, inl Ax>
fi ;\mlambda{}i,x. let A,B,$_{}$ = x in
<let v1,v2 = cover-seq(\%2;a;b;(i + 1) - 1)
in case \%2 (v1 + v2/r(2)) of inl(x) => x | inr(y) => A
, let v1,v2 = cover-seq(\%2;a;b;(i + 1) - 1)
in case \%2 (v1 + v2/r(2)) of inl(x) => B | inr(y) => y
, let v1,v2 = cover-seq(\%2;a;b;i + 1)
in if \%2 (v1 + v2/r(2)) then inr Ax else inl Ax fi >))\000C)
, \mlambda{}n.let \%11,\%13,\%14 = primrec(n;if \%2 (a + b/r(2))
then <\%3, \%2@0, inr Ax >
else <\%3, \%2@0, inl Ax>
fi ;\mlambda{}i,x. let A,B,$_{}$ = x in
<let v1,v2 = cover-seq(\%2;a;b;(i + 1) - 1)
in case \%2 (v1 + v2/r(2))
of inl(x) =>
x
| inr(y) =>
A
, let v1,v2 = cover-seq(\%2;a;b;(i + 1) - 1)
in case \%2 (v1 + v2/r(2))
of inl(x) =>
B
| inr(y) =>
y
, let v1,v2 = cover-seq(\%2;a;b;i + 1)
in if \%2 (v1 + v2/r(2))
then inr Ax
else inl Ax
fi >) in
\%13
, \mlambda{}k.(log(2;(4 * k) * (x + 1)) + 1)
, \mlambda{}k.imax(log(2;(4 * 2 * k) * (x + 1)) + 1;log(2;(2 * k) * (x + 1)))>
Home
Index