### Nuprl Lemma : Taylor-remainder_wf

`∀[I:Interval]. ∀[n:ℕ]. ∀[F:ℕn + 1 ⟶ I ⟶ℝ]. ∀[b,a:{a:ℝ| a ∈ I} ].  (Taylor-remainder(I;n;b;a;i,x.F[i;x]) ∈ ℝ)`

Proof

Definitions occuring in Statement :  Taylor-remainder: `Taylor-remainder(I;n;b;a;i,x.F[i; x])` rfun: `I ⟶ℝ` i-member: `r ∈ I` interval: `Interval` real: `ℝ` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` member: `t ∈ T` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  so_apply: `x[s]` so_lambda: `λ2x.t[x]` rfun: `I ⟶ℝ` label: `...\$L... t` so_lambda: `λ2x y.t[x; y]` subtype_rel: `A ⊆r B` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` all: `∀x:A. B[x]` ge: `i ≥ j ` nat: `ℕ` prop: `ℙ` implies: `P `` Q` not: `¬A` false: `False` less_than': `less_than'(a;b)` le: `A ≤ B` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` so_apply: `x[s1;s2]` Taylor-remainder: `Taylor-remainder(I;n;b;a;i,x.F[i; x])` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  rsub_wf false_wf nat_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf lelt_wf i-member_wf Taylor-approx_wf rfun_wf real_wf int_seg_wf set_wf nat_wf interval_wf
Rules used in proof :  functionEquality equalitySymmetry equalityTransitivity axiomEquality setEquality because_Cache computeAll voidEquality voidElimination isect_memberEquality intEquality int_eqEquality lambdaEquality dependent_pairFormation independent_isectElimination unionElimination addEquality dependent_functionElimination hypothesis lambdaFormation independent_pairFormation natural_numberEquality dependent_set_memberEquality hypothesisEquality applyEquality isectElimination sqequalHypSubstitution lemma_by_obid sqequalRule rename thin setElimination cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[I:Interval].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:\mBbbN{}n  +  1  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[b,a:\{a:\mBbbR{}|  a  \mmember{}  I\}  ].
(Taylor-remainder(I;n;b;a;i,x.F[i;x])  \mmember{}  \mBbbR{})

Date html generated: 2016_05_18-AM-10_30_14
Last ObjectModification: 2016_01_17-AM-00_23_07

Theory : reals

Home Index