### Nuprl Lemma : fun-converges-rmul

`∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ.`
`  (λn.f[n;x]↓ for x ∈ I) `` (∀g:I ⟶ℝ. (g[x] continuous for x ∈ I `` λn.f[n;x] * g[x]↓ for x ∈ I))))`

Proof

Definitions occuring in Statement :  fun-converges: `λn.f[n; x]↓ for x ∈ I)` continuous: `f[x] continuous for x ∈ I` rfun: `I ⟶ℝ` interval: `Interval` rmul: `a * b` nat: `ℕ` so_apply: `x[s1;s2]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` rfun: `I ⟶ℝ` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` uall: `∀[x:A]. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` so_apply: `x[s]` rev_implies: `P `` Q` fun-cauchy: `λn.f[n; x] is cauchy for x ∈ I` so_lambda: `λ2x.t[x]` label: `...\$L... t` nat_plus: `ℕ+` exists: `∃x:A. B[x]` uimplies: `b supposing a` subinterval: `I ⊆ J ` guard: `{T}` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` rneq: `x ≠ y` or: `P ∨ Q` int_upper: `{i...}` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top` le: `A ≤ B` uiff: `uiff(P;Q)` cand: `A c∧ B` sq_stable: `SqStable(P)` squash: `↓T`
Lemmas referenced :  fun-converges-iff-cauchy nat_wf i-member_wf real_wf rmul_wf rfun_wf nat_plus_wf set_wf icompact_wf i-approx_wf continuous_wf fun-converges_wf interval_wf i-approx-is-subinterval less_than_wf continuous_functionality_wrt_subinterval r-bound_wf Inorm_wf subtype_rel_sets all_wf rleq_wf rabs_wf int-to-real_wf Inorm-bound rfun_subtype r-bound-property rleq_functionality_wrt_implies rleq_weakening_equal mul_nat_plus int_upper_wf rsub_wf int_upper_subtype_nat nat_plus_subtype_nat rdiv_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 uiff_transitivity rleq_functionality rabs_functionality req_inversion rmul-rsub-distrib req_weakening rabs-rmul mul_bounds_1b zero-rleq-rabs rleq-int sq_stable__icompact decidable__le intformle_wf int_formula_prop_le_lemma multiply_nat_plus itermMultiply_wf intformeq_wf int_term_value_mul_lemma int_formula_prop_eq_lemma equal_wf rmul_functionality_wrt_rleq2 rmul_comm rleq-int-fractions rmul-int-rdiv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality sqequalRule lambdaEquality applyEquality functionExtensionality hypothesis because_Cache setElimination rename dependent_set_memberEquality isectElimination setEquality productElimination independent_functionElimination functionEquality natural_numberEquality dependent_pairFormation independent_isectElimination equalityTransitivity equalitySymmetry inrFormation unionElimination int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll multiplyEquality inlFormation imageMemberEquality baseClosed imageElimination productEquality applyLambdaEquality

Latex:
\mforall{}I:Interval.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}.
(\mlambda{}n.f[n;x]\mdownarrow{}  for  x  \mmember{}  I)  {}\mRightarrow{}  (\mforall{}g:I  {}\mrightarrow{}\mBbbR{}.  (g[x]  continuous  for  x  \mmember{}  I  {}\mRightarrow{}  \mlambda{}n.f[n;x]  *  g[x]\mdownarrow{}  for  x  \mmember{}  I))))

Date html generated: 2017_10_03-PM-00_03_04
Last ObjectModification: 2017_07_28-AM-08_31_24

Theory : reals

Home Index