Nuprl Lemma : fun-converges-to-rminus

I:Interval. ∀f:ℕ ⟶ I ⟶ℝ. ∀g:I ⟶ℝ.  (lim n→∞.f[n;x] = λy.g[y] for x ∈  lim n→∞.-(f[n;x]) = λy.-(g[y]) for x ∈ I)


Proof




Definitions occuring in Statement :  fun-converges-to: lim n→∞.f[n; x] = λy.g[y] for x ∈ I rfun: I ⟶ℝ interval: Interval rminus: -(x) nat: so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q fun-converges-to: lim n→∞.f[n; x] = λy.g[y] for x ∈ I member: t ∈ T nat_plus: + uall: [x:A]. B[x] prop: exists: x:A. B[x] so_lambda: λ2x.t[x] so_apply: x[s] so_apply: x[s1;s2] subtype_rel: A ⊆B rfun: I ⟶ℝ uimplies: supposing a rneq: x ≠ y guard: {T} or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q int_upper: {i...} decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top so_lambda: λ2y.t[x; y] label: ...$L... t subinterval: I ⊆  le: A ≤ B rsub: y uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) true: True squash: T
Lemmas referenced :  i-approx-is-subinterval less_than_wf int_upper_wf set_wf real_wf i-member_wf i-approx_wf all_wf rleq_wf rabs_wf rsub_wf rminus_wf int_upper_subtype_nat nat_plus_subtype_nat rdiv_wf int-to-real_wf rless-int int_upper_properties nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf rless_wf nat_plus_wf icompact_wf fun-converges-to_wf nat_wf rfun_wf interval_wf req_wf subtype_rel_sets radd_wf rmul_wf req_weakening uiff_transitivity req_functionality rminus-radd radd_functionality rminus-rminus radd_comm rminus-as-rmul rmul_functionality req_inversion req_transitivity uiff_transitivity2 rleq_functionality rabs_functionality squash_wf true_wf rabs-rminus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality cut introduction extract_by_obid dependent_set_memberEquality setElimination rename hypothesis isectElimination natural_numberEquality productElimination dependent_pairFormation sqequalRule lambdaEquality because_Cache setEquality applyEquality functionExtensionality independent_isectElimination inrFormation independent_functionElimination unionElimination int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll functionEquality minusEquality imageElimination equalityTransitivity equalitySymmetry imageMemberEquality baseClosed

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.  \mforall{}g:I  {}\mrightarrow{}\mBbbR{}.
    (lim  n\mrightarrow{}\minfty{}.f[n;x]  =  \mlambda{}y.g[y]  for  x  \mmember{}  I  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.-(f[n;x])  =  \mlambda{}y.-(g[y])  for  x  \mmember{}  I)



Date html generated: 2016_10_26-AM-11_13_43
Last ObjectModification: 2016_08_28-PM-06_43_55

Theory : reals


Home Index