### Nuprl Lemma : converges-to_functionality

`∀x1,x2:ℕ ⟶ ℝ. ∀y1,y2:ℝ.  ({lim n→∞.x1[n] = y1 `` lim n→∞.x2[n] = y2}) supposing ((y1 = y2) and (∀n:ℕ. (x1[n] = x2[n])))`

Proof

Definitions occuring in Statement :  converges-to: `lim n→∞.x[n] = y` req: `x = y` real: `ℝ` nat: `ℕ` uimplies: `b supposing a` guard: `{T}` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  guard: `{T}` all: `∀x:A. B[x]` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s]` implies: `P `` Q` converges-to: `lim n→∞.x[n] = y` nat_plus: `ℕ+` rneq: `x ≠ y` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` sq_exists: `∃x:{A| B[x]}` nat: `ℕ` ge: `i ≥ j ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` prop: `ℙ` so_lambda: `λ2x.t[x]` uiff: `uiff(P;Q)`
Lemmas referenced :  req_weakening rsub_functionality rabs_functionality rleq_functionality rsub_wf rabs_wf rleq_wf le_wf real_wf all_wf req_wf converges-to_wf nat_plus_wf rless_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformless_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__lt nat_plus_properties nat_properties rless-int int-to-real_wf rdiv_wf nat_wf req_witness
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation isect_memberFormation cut introduction sqequalHypSubstitution lambdaEquality dependent_functionElimination thin hypothesisEquality lemma_by_obid isectElimination applyEquality independent_functionElimination hypothesis rename natural_numberEquality setElimination independent_isectElimination inrFormation because_Cache productElimination unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll promote_hyp functionEquality dependent_set_memberEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}x1,x2:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}y1,y2:\mBbbR{}.
(\{lim  n\mrightarrow{}\minfty{}.x1[n]  =  y1  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x2[n]  =  y2\})  supposing  ((y1  =  y2)  and  (\mforall{}n:\mBbbN{}.  (x1[n]  =  x2[n])))

Date html generated: 2016_05_18-AM-07_35_42
Last ObjectModification: 2016_01_17-AM-02_02_40

Theory : reals

Home Index