Nuprl Lemma : common-limit-squeeze-ext
∀a,b,c:ℕ ⟶ ℝ.
((∀n:ℕ. ((a[n] ≤ a[n + 1]) ∧ (a[n + 1] ≤ b[n + 1]) ∧ (b[n + 1] ≤ b[n])))
⇒ lim n→∞.c[n] = r0
⇒ (∀n:ℕ. r0≤b[n] - a[n]≤c[n])
⇒ (∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)))
Proof
Definitions occuring in Statement :
converges-to: lim n→∞.x[n] = y,
rbetween: x≤y≤z,
rleq: x ≤ y,
rsub: x - y,
int-to-real: r(n),
real: ℝ,
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
so_apply: x[s],
so_lambda: λ2x.t[x],
accelerate: accelerate(k;f),
imax: imax(a;b),
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
bnot: ¬bb,
lt_int: i <z j,
btrue: tt,
it: ⋅,
bfalse: ff,
common-limit-squeeze,
converges-iff-cauchy,
sq-all-large-and,
uall: ∀[x:A]. B[x],
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),
so_apply: x[s1;s2;s3;s4],
top: Top,
uimplies: b supposing a
Lemmas referenced :
common-limit-squeeze,
lifting-strict-decide,
istype-void,
strict4-decide,
lifting-strict-less,
converges-iff-cauchy,
sq-all-large-and
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry,
isectElimination,
baseClosed,
isect_memberEquality_alt,
voidElimination,
independent_isectElimination
Latex:
\mforall{}a,b,c:\mBbbN{} {}\mrightarrow{} \mBbbR{}.
((\mforall{}n:\mBbbN{}. ((a[n] \mleq{} a[n + 1]) \mwedge{} (a[n + 1] \mleq{} b[n + 1]) \mwedge{} (b[n + 1] \mleq{} b[n])))
{}\mRightarrow{} lim n\mrightarrow{}\minfty{}.c[n] = r0
{}\mRightarrow{} (\mforall{}n:\mBbbN{}. r0\mleq{}b[n] - a[n]\mleq{}c[n])
{}\mRightarrow{} (\mexists{}y:\mBbbR{}. (lim n\mrightarrow{}\minfty{}.a[n] = y \mwedge{} lim n\mrightarrow{}\minfty{}.b[n] = y)))
Date html generated:
2019_10_29-AM-10_11_05
Last ObjectModification:
2019_04_01-PM-10_59_20
Theory : reals
Home
Index