### Nuprl Lemma : derivative_functionality_wrt_subinterval

`∀I,J:Interval.  ∀[f,f':I ⟶ℝ].  (J ⊆ I  `` d(f[x])/dx = λx.f'[x] on I `` d(f[x])/dx = λx.f'[x] on J)`

Proof

Definitions occuring in Statement :  derivative: `d(f[x])/dx = λz.g[z] on I` subinterval: `I ⊆ J ` rfun: `I ⟶ℝ` interval: `Interval` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` implies: `P `` Q` derivative: `d(f[x])/dx = λz.g[z] on I` member: `t ∈ T` and: `P ∧ Q` prop: `ℙ` nat_plus: `ℕ+` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` label: `...\$L... t` rfun: `I ⟶ℝ` cand: `A c∧ B` iproper: `iproper(I)` uimplies: `b supposing a` subinterval: `I ⊆ J ` rbetween: `x≤y≤z` guard: `{T}` sq_exists: `∃x:{A| B[x]}` rneq: `x ≠ y` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rless: `x < y` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top`
Lemmas referenced :  compact-subinterval i-approx_wf icompact_wf subinterval_transitivity less_than_wf i-approx-is-subinterval set_wf nat_plus_wf iproper_wf derivative_wf i-member_wf real_wf subinterval_wf rfun_wf interval_wf i-finite_wf i-finite-subinterval i-member-finite left-endpoint_wf i-approx-finite icompact-endpoints right-endpoint_wf rless_transitivity2 rless_transitivity1 i-member-approx rless_wf int-to-real_wf all_wf rleq_wf rabs_wf rsub_wf rmul_wf rdiv_wf rless-int 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
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation sqequalHypSubstitution cut hypothesis dependent_functionElimination thin hypothesisEquality introduction extract_by_obid setElimination rename dependent_set_memberEquality isectElimination productElimination independent_functionElimination natural_numberEquality because_Cache sqequalRule lambdaEquality productEquality applyEquality setEquality independent_pairFormation independent_isectElimination promote_hyp functionEquality inrFormation unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll

Latex:
\mforall{}I,J:Interval.    \mforall{}[f,f':I  {}\mrightarrow{}\mBbbR{}].    (J  \msubseteq{}  I    {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I  {}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  J)

Date html generated: 2016_10_26-AM-11_19_12
Last ObjectModification: 2016_08_22-PM-10_08_15

Theory : reals

Home Index