Nuprl Lemma : subsequence-mconverges
∀[X:Type]. ∀[d:metric(X)]. ∀[a:X]. ∀x,y:ℕ ⟶ X. (subsequence(a,b.a ≡ b;n.x[n];n.y[n]) ⇒ x[n]↓ as n→∞ ⇒ y[n]↓ as n→∞)
Proof
Definitions occuring in Statement :
mconverges: x[n]↓ as n→∞,
meq: x ≡ y,
metric: metric(X),
subsequence: subsequence(a,b.E[a; b];m.x[m];n.y[n]),
nat: ℕ,
uall: ∀[x:A]. B[x],
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x],
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
mconverges: x[n]↓ as n→∞,
exists: ∃x:A. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
so_apply: x[s],
metric: metric(X),
prop: ℙ,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2]
Lemmas referenced :
subsequence-mconverges-to,
istype-nat,
mconverges-to_wf,
mconverges_wf,
subsequence_wf,
meq_wf,
metric_wf,
istype-universe
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
lambdaFormation_alt,
sqequalHypSubstitution,
productElimination,
thin,
dependent_pairFormation_alt,
hypothesisEquality,
cut,
introduction,
extract_by_obid,
isectElimination,
because_Cache,
dependent_functionElimination,
sqequalRule,
lambdaEquality_alt,
applyEquality,
hypothesis,
independent_functionElimination,
universeIsType,
setElimination,
rename,
inhabitedIsType,
functionIsType,
instantiate,
universeEquality
Latex:
\mforall{}[X:Type]. \mforall{}[d:metric(X)]. \mforall{}[a:X].
\mforall{}x,y:\mBbbN{} {}\mrightarrow{} X. (subsequence(a,b.a \mequiv{} b;n.x[n];n.y[n]) {}\mRightarrow{} x[n]\mdownarrow{} as n\mrightarrow{}\minfty{} {}\mRightarrow{} y[n]\mdownarrow{} as n\mrightarrow{}\minfty{})
Date html generated:
2019_10_30-AM-06_40_49
Last ObjectModification:
2019_10_02-AM-10_53_33
Theory : reals
Home
Index