Nuprl Lemma : series-diverges_functionality
∀[x,y:ℕ ⟶ ℝ]. {Σn.x[n]↑ ⇒ Σn.y[n]↑} supposing ∀n:ℕ. (x[n] = y[n])
Proof
Definitions occuring in Statement :
series-diverges: Σn.x[n]↑,
req: x = y,
real: ℝ,
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
uiff: uiff(P;Q),
not: ¬A,
false: False,
less_than': less_than'(a;b),
le: A ≤ B,
subtype_rel: A ⊆r B,
so_lambda: λ2x.t[x],
nat: ℕ,
cand: A c∧ B,
prop: ℙ,
and: P ∧ Q,
exists: ∃x:A. B[x],
diverges: n.x[n]↑,
series-diverges: Σn.x[n]↑,
guard: {T},
implies: P ⇒ Q,
so_apply: x[s],
all: ∀x:A. B[x],
member: t ∈ T,
uimplies: b supposing a,
uall: ∀[x:A]. B[x]
Lemmas referenced :
rsum_functionality2,
rsub_functionality,
rabs_functionality,
req_weakening,
rleq_functionality,
real_wf,
req_wf,
series-diverges_wf,
all_wf,
int-to-real_wf,
rless_wf,
exists_wf,
int_seg_wf,
false_wf,
int_seg_subtype_nat,
rsum_wf,
rsub_wf,
rabs_wf,
rleq_wf,
le_wf,
nat_wf,
req_witness
Rules used in proof :
intEquality,
dependent_set_memberEquality,
functionEquality,
independent_isectElimination,
addEquality,
natural_numberEquality,
because_Cache,
setElimination,
productEquality,
promote_hyp,
independent_pairFormation,
dependent_pairFormation,
productElimination,
lambdaFormation,
rename,
independent_functionElimination,
hypothesis,
functionExtensionality,
applyEquality,
isectElimination,
extract_by_obid,
hypothesisEquality,
thin,
dependent_functionElimination,
lambdaEquality,
sqequalHypSubstitution,
sqequalRule,
introduction,
cut,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[x,y:\mBbbN{} {}\mrightarrow{} \mBbbR{}]. \{\mSigma{}n.x[n]\muparrow{} {}\mRightarrow{} \mSigma{}n.y[n]\muparrow{}\} supposing \mforall{}n:\mBbbN{}. (x[n] = y[n])
Date html generated:
2016_11_08-AM-09_00_41
Last ObjectModification:
2016_11_07-PM-00_01_23
Theory : reals
Home
Index