Nuprl Lemma : simple-chain-rule

`∀I:Interval. ∀f,f':I ⟶ℝ. ∀g,g':(-∞, ∞) ⟶ℝ.`
`  (iproper(I)`
`  `` (∀x,y:{x:ℝ| x ∈ I} .  ((x = y) `` (f'[x] = f'[y])))`
`  `` (∀x,y:ℝ.  ((x = y) `` (g'[x] = g'[y])))`
`  `` d(f[x])/dx = λx.f'[x] on I`
`  `` d(g[x])/dx = λx.g'[x] on (-∞, ∞)`
`  `` 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` rfun: `I ⟶ℝ` riiint: `(-∞, ∞)` 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` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` label: `...\$L... t` rfun: `I ⟶ℝ` top: `Top` true: `True` guard: `{T}`
Lemmas referenced :  chain-rule riiint_wf iproper-riiint req_wf set_wf real_wf i-member_wf derivative_wf all_wf member_riiint_lemma true_wf iproper_wf rfun_wf interval_wf continuous-maps-compact differentiable-continuous
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination isectElimination setElimination rename sqequalRule lambdaEquality applyEquality dependent_set_memberEquality setEquality because_Cache functionEquality isect_memberEquality voidElimination voidEquality natural_numberEquality

Latex:
\mforall{}I:Interval.  \mforall{}f,f':I  {}\mrightarrow{}\mBbbR{}.  \mforall{}g,g':(-\minfty{},  \minfty{})  {}\mrightarrow{}\mBbbR{}.
(iproper(I)
{}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (f'[x]  =  f'[y])))
{}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.    ((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  (-\minfty{},  \minfty{})
{}\mRightarrow{}  d(g[f[x]])/dx  =  \mlambda{}x.g'[f[x]]  *  f'[x]  on  I)

Date html generated: 2016_10_26-AM-11_30_55
Last ObjectModification: 2016_09_06-AM-10_02_48

Theory : reals

Home Index