---

Step * of Lemma derivative_functionality2

∀I,J:Interval.
  ∀[f1,f2,g1,g2:I ⟶ℝ].
    (rfun-eq(I;f1;f2) ⇒ rfun-eq(I;g1;g2) ⇒ J ⊆ I  ⇒ d(f1[x])/dx = λx.g1[x] on I ⇒ d(f2[x])/dx = λx.g2[x] on J)
BY
{ xxx(Auto
      THEN (Assert d(f2[x])/dx = λx.g2[x] on I BY
                  (DerivativeFunctionality (-1) THEN Auto THEN RepeatFor 2 ((D 7 With ⌜x⌝  THEN Auto))))
      THEN UsingVars [`J'] (FLemma `derivative_functionality_wrt_subinterval` [-1])
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}I,J:Interval.
    \mforall{}[f1,f2,g1,g2:I  {}\mrightarrow{}\mBbbR{}].
        (rfun-eq(I;f1;f2)
        {}\mRightarrow{}  rfun-eq(I;g1;g2)
        {}\mRightarrow{}  J  \msubseteq{}  I 
        {}\mRightarrow{}  d(f1[x])/dx  =  \mlambda{}x.g1[x]  on  I
        {}\mRightarrow{}  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  J)


By

---

Latex:
xxx(Auto
        THEN  (Assert  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  I  BY
                                (DerivativeFunctionality  (-1)
                                  THEN  Auto
                                  THEN  RepeatFor  2  ((D  7  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto))))
        THEN  UsingVars  [`J']  (FLemma  `derivative\_functionality\_wrt\_subinterval`  [-1])
        THEN  Auto)xxx

---

Home Index