### Nuprl Lemma : chain-rule

`∀I,J:Interval. ∀f,f':I ⟶ℝ. ∀g,g':J ⟶ℝ.`
`  (iproper(J)`
`  `` maps-compact(I;J;x.f[x])`
`  `` (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) `` (f'[x] = f'[y])))`
`  `` (∀x,y:{x:ℝ| x ∈ J} .  ((x = y) `` (g'[x] = g'[y])))`
`  `` d(f[x])/dx = λx.f'[x] on I`
`  `` d(g[x])/dx = λx.g'[x] on J`
`  `` d(g[f[x]])/dx = λx.g'[f[x]] * f'[x] on I)`

Proof

Definitions occuring in Statement :  derivative: `d(f[x])/dx = λz.g[z] on I` maps-compact: `maps-compact(I;J;x.f[x])` rfun: `I ⟶ℝ` i-member: `r ∈ I` iproper: `iproper(I)` interval: `Interval` req: `x = y` rmul: `a * b` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} `
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` implies: `P `` Q` so_lambda: `λ2x.t[x]` rfun: `I ⟶ℝ` so_apply: `x[s]` uall: `∀[x:A]. B[x]` prop: `ℙ` label: `...\$L... t`
Lemmas referenced :  chain-rule_0 function-proper-continuous i-member_wf real_wf derivative_wf all_wf req_wf maps-compact_wf iproper_wf rfun_wf interval_wf differentiable-continuous
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination because_Cache sqequalRule lambdaEquality applyEquality setElimination rename dependent_set_memberEquality isectElimination setEquality functionEquality

Latex:
\mforall{}I,J:Interval.  \mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.  \mforall{}g,g':J  {}\mrightarrow{}\mBbbR{}.
(iproper(J)
{}\mRightarrow{}  maps-compact(I;J;x.f[x])
{}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
{}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  J\}  .    ((x  =  y)  {}\mRightarrow{}  (g'[x]  =  g'[y])))
{}\mRightarrow{}  d(f[x])/dx  =  \mlambda{}x.f'[x]  on  I
{}\mRightarrow{}  d(g[x])/dx  =  \mlambda{}x.g'[x]  on  J
{}\mRightarrow{}  d(g[f[x]])/dx  =  \mlambda{}x.g'[f[x]]  *  f'[x]  on  I)

Date html generated: 2016_10_26-AM-11_30_38
Last ObjectModification: 2016_09_05-AM-10_09_21

Theory : reals

Home Index