### Nuprl Lemma : fun-converges_functionality

`∀[I:Interval]. ∀f,g:ℕ ⟶ I ⟶ℝ.  ((∀n:ℕ. rfun-eq(I;f n;g n)) `` λn.f[n;x]↓ for x ∈ I) `` λn.g[n;x]↓ for x ∈ I))`

Proof

Definitions occuring in Statement :  fun-converges: `λn.f[n; x]↓ for x ∈ I)` rfun-eq: `rfun-eq(I;f;g)` rfun: `I ⟶ℝ` interval: `Interval` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_lambda: `λ2x y.t[x; y]` label: `...\$L... t` rfun: `I ⟶ℝ` so_apply: `x[s1;s2]` subtype_rel: `A ⊆r B` prop: `ℙ` nat_plus: `ℕ+` uimplies: `b supposing a` sq_stable: `SqStable(P)` guard: `{T}` squash: `↓T` fun-converges: `λn.f[n; x]↓ for x ∈ I)` exists: `∃x:A. B[x]` fun-converges-to: `lim n→∞.f[n; x] = λy.g[y] for x ∈ I` rneq: `x ≠ y` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` int_upper: `{i...}` decidable: `Dec(P)` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s]` le: `A ≤ B` rfun-eq: `rfun-eq(I;f;g)` r-ap: `f(x)` uiff: `uiff(P;Q)`
Lemmas referenced :  fun-converges_wf subtype_rel_self real_wf i-member_wf istype-nat rfun-eq_wf rfun_wf interval_wf upper_subtype_nat sq_stable__le le_weakening2 istype-int_upper i-approx_wf istype-less_than i-member-approx rleq_wf rabs_wf rsub_wf rdiv_wf rless-int int_upper_properties nat_plus_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf istype-int int_formula_prop_and_lemma istype-void 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 int-to-real_wf nat_plus_wf icompact_wf fun-converges-to_wf sq_stable__rleq rleq_functionality rabs_functionality rsub_functionality req_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt lambdaFormation_alt universeIsType cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule lambdaEquality_alt applyEquality hypothesis functionEquality setEquality setIsType functionIsType inhabitedIsType dependent_functionElimination setElimination rename independent_isectElimination natural_numberEquality independent_functionElimination imageMemberEquality baseClosed imageElimination because_Cache dependent_set_memberEquality_alt productElimination dependent_pairFormation_alt inrFormation_alt unionElimination approximateComputation int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation closedConclusion

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

Date html generated: 2019_10_30-AM-08_57_35
Last ObjectModification: 2018_11_12-AM-10_57_07

Theory : reals

Home Index