Nuprl Lemma : Taylor-approx_functionality

[I:Interval]. ∀[n:ℕ]. ∀[F:ℕ1 ⟶ I ⟶ℝ].
  ∀[a1,b1,a2,b2:{a:ℝa ∈ I} ].
    (Taylor-approx(n;a1;b1;i,x.F[i;x]) Taylor-approx(n;a2;b2;i,x.F[i;x])) supposing ((a1 a2) and (b1 b2)) 
  supposing ∀k:ℕ1. ∀x,y:{a:ℝa ∈ I} .  ((x y)  (F[k;x] F[k;y]))


Definitions occuring in Statement :  Taylor-approx: Taylor-approx(n;a;b;i,x.F[i; x]) rfun: I ⟶ℝ i-member: r ∈ I interval: Interval req: y real: int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] all: x:A. B[x] implies:  Q set: {x:A| B[x]}  function: x:A ⟶ B[x] add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a Taylor-approx: Taylor-approx(n;a;b;i,x.F[i; x]) so_lambda: λ2x.t[x] so_apply: x[s1;s2] subtype_rel: A ⊆B nat: le: A ≤ B and: P ∧ Q less_than': less_than'(a;b) false: False not: ¬A implies:  Q prop: rneq: x ≠ y guard: {T} or: P ∨ Q all: x:A. B[x] iff: ⇐⇒ Q rev_implies:  Q int_seg: {i..j-} ge: i ≥  lelt: i ≤ j < k decidable: Dec(P) nat_plus: + satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top so_apply: x[s] pointwise-req: x[k] y[k] for k ∈ [n,m] so_lambda: λ2y.t[x; y] label: ...$L... t rfun: I ⟶ℝ
Lemmas referenced :  rsum_functionality rmul_wf rdiv_wf int-to-real_wf fact_wf int_seg_subtype_nat false_wf rless-int int_seg_properties nat_properties decidable__lt le_wf nat_plus_properties satisfiable-full-omega-tt intformand_wf intformless_wf itermConstant_wf itermVar_wf intformnot_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_wf rless_wf rnexp_wf rsub_wf rmul_functionality itermAdd_wf intformle_wf int_term_value_add_lemma int_formula_prop_le_lemma lelt_wf i-member_wf rnexp_functionality rsub_functionality req_witness Taylor-approx_wf int_seg_wf rfun_wf real_wf req_wf set_wf all_wf nat_wf interval_wf req_weakening rdiv_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality because_Cache sqequalRule lambdaEquality applyEquality functionExtensionality hypothesisEquality hypothesis setElimination rename dependent_set_memberEquality addEquality independent_isectElimination independent_pairFormation lambdaFormation inrFormation dependent_functionElimination productElimination independent_functionElimination unionElimination equalityTransitivity equalitySymmetry Error :applyLambdaEquality,  voidElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidEquality computeAll setEquality functionEquality

\mforall{}[I:Interval].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:\mBbbN{}n  +  1  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}].
    \mforall{}[a1,b1,a2,b2:\{a:\mBbbR{}|  a  \mmember{}  I\}  ].
        (Taylor-approx(n;a1;b1;i,x.F[i;x])  =  Taylor-approx(n;a2;b2;i,x.F[i;x]))  supposing 
              ((a1  =  a2)  and 
              (b1  =  b2)) 
    supposing  \mforall{}k:\mBbbN{}n  +  1.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (F[k;x]  =  F[k;y]))

Date html generated: 2016_10_26-AM-11_44_27
Last ObjectModification: 2016_08_28-PM-10_37_45

Theory : reals

Home Index