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])))


Definitions occuring in Statement :  converges-to: lim n→∞.x[n] y req: y real: nat: uimplies: supposing a guard: {T} so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x]
Definitions unfolded in proof :  guard: {T} all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x] so_apply: x[s] implies:  Q converges-to: lim n→∞.x[n] y nat_plus: + rneq: x ≠ y or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q sq_exists: x:{A| B[x]} nat: ge: i ≥  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

\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