Nuprl Lemma : converges-iff-cauchy-ext
∀x:ℕ ⟶ ℝ. (x[n]↓ as n→∞ ⇐⇒ cauchy(n.x[n]))
Proof
Definitions occuring in Statement :
cauchy: cauchy(n.x[n]),
converges: x[n]↓ as n→∞,
real: ℝ,
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
member: t ∈ T,
so_apply: x[s],
accelerate: accelerate(k;f),
converges-iff-cauchy
Lemmas referenced :
converges-iff-cauchy
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry,
callbyvalueReduce,
sqleReflexivity
Latex:
\mforall{}x:\mBbbN{} {}\mrightarrow{} \mBbbR{}. (x[n]\mdownarrow{} as n\mrightarrow{}\minfty{} \mLeftarrow{}{}\mRightarrow{} cauchy(n.x[n]))
Date html generated:
2019_10_29-AM-10_10_10
Last ObjectModification:
2019_04_01-PM-10_59_39
Theory : reals
Home
Index