Nuprl Lemma : common-limit-midpoints
∀a,b:ℕ ⟶ ℝ.
((∀n:ℕ
(((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n]))))
⇒ (∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)))
Proof
Definitions occuring in Statement :
converges-to: lim n→∞.x[n] = y,
rdiv: (x/y),
req: x = y,
radd: a + b,
int-to-real: r(n),
real: ℝ,
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
uall: ∀[x:A]. B[x],
member: t ∈ T,
nat: ℕ,
false: False,
ge: i ≥ j ,
uimplies: b supposing a,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
and: P ∧ Q,
prop: ℙ,
rleq: x ≤ y,
rnonneg: rnonneg(x),
le: A ≤ B,
decidable: Dec(P),
or: P ∨ Q,
squash: ↓T,
true: True,
subtype_rel: A ⊆r B,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
less_than': less_than'(a;b),
less_than: a < b,
so_apply: x[s],
rneq: x ≠ y,
rless: x < y,
sq_exists: ∃x:A [B[x]],
nat_plus: ℕ+,
rev_uimplies: rev_uimplies(P;Q),
int_nzero: ℤ-o,
nequal: a ≠ b ∈ T ,
sq_type: SQType(T),
req_int_terms: t1 ≡ t2,
rdiv: (x/y),
rge: x ≥ y,
cand: A c∧ B,
absval: |i|,
so_lambda: λ2x.t[x],
real: ℝ,
int_upper: {i...},
converges: x[n]↓ as n→∞,
cauchy: cauchy(n.x[n]),
top: Top,
converges-to: lim n→∞.x[n] = y,
sq-all-large: ∀large(n).{P[n]}
Latex:
\mforall{}a,b:\mBbbN{} {}\mrightarrow{} \mBbbR{}.
((\mforall{}n:\mBbbN{}
(((a[n + 1] = a[n]) \mwedge{} (b[n + 1] = (a[n] + b[n]/r(2))))
\mvee{} ((a[n + 1] = (a[n] + b[n]/r(2))) \mwedge{} (b[n + 1] = b[n]))))
{}\mRightarrow{} (\mexists{}y:\mBbbR{}. (lim n\mrightarrow{}\minfty{}.a[n] = y \mwedge{} lim n\mrightarrow{}\minfty{}.b[n] = y)))
Date html generated:
2020_05_20-AM-11_10_09
Last ObjectModification:
2019_12_14-AM-11_19_06
Theory : reals
Home
Index