Nuprl Lemma : converges-absolutely-converges
∀x:ℕ ⟶ ℝ. (converges-absolutely(n.x[n]) ⇒ Σn.x[n]↓)
Proof
Definitions occuring in Statement :
converges-absolutely: converges-absolutely(n.x[n]),
series-converges: Σn.x[n]↓,
real: ℝ,
nat: ℕ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
converges-absolutely: converges-absolutely(n.x[n]),
all: ∀x:A. B[x],
implies: P ⇒ Q,
so_lambda: λ2x.t[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_apply: x[s],
uimplies: b supposing a,
prop: ℙ
Lemmas referenced :
comparison-test,
rabs_wf,
nat_wf,
rleq_weakening_equal,
series-converges_wf,
real_wf
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lambdaFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
lambdaEquality,
isectElimination,
applyEquality,
hypothesisEquality,
hypothesis,
independent_functionElimination,
independent_isectElimination,
because_Cache,
functionEquality
Latex:
\mforall{}x:\mBbbN{} {}\mrightarrow{} \mBbbR{}. (converges-absolutely(n.x[n]) {}\mRightarrow{} \mSigma{}n.x[n]\mdownarrow{})
Date html generated:
2016_05_18-AM-08_00_07
Last ObjectModification:
2015_12_28-AM-01_10_24
Theory : reals
Home
Index