---

Step * of Lemma Taylor-approx_functionality

∀[I:Interval]. ∀[n:ℕ]. ∀[F:ℕn + 1 ⟶ I ⟶ℝ].
  ∀[a1,b1,a2,b2:{a:ℝ| a ∈ I} ].
    (Taylor-approx(n;a1;b1;i,x.F[i;x]) = Taylor-approx(n;a2;b2;i,x.F[i;x])) supposing ((a1 = a2) and (b1 = b2)) 
  supposing ∀k:ℕn + 1. ∀x,y:{a:ℝ| a ∈ I} .  ((x = y) ⇒ (F[k;x] = F[k;y]))
BY
{ (Auto
   THEN Unfold `Taylor-approx` 0
   THEN BLemma `rsum_functionality`
   THEN Auto
   THEN D 0
   THEN Auto
   THEN BLemma `rmul_functionality`
   THEN Auto
   THEN (BLemma `rdiv_functionality` ORELSE BLemma `rnexp_functionality`)
   THEN Auto
   THEN Try ((BLemma `rsub_functionality`⋅ THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[I:Interval].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:\mBbbN{}n  +  1  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}].
    \mforall{}[a1,b1,a2,b2:\{a:\mBbbR{}|  a  \mmember{}  I\}  ].
        (Taylor-approx(n;a1;b1;i,x.F[i;x])  =  Taylor-approx(n;a2;b2;i,x.F[i;x]))  supposing 
              ((a1  =  a2)  and 
              (b1  =  b2)) 
    supposing  \mforall{}k:\mBbbN{}n  +  1.  \mforall{}x,y:\{a:\mBbbR{}|  a  \mmember{}  I\}  .    ((x  =  y)  {}\mRightarrow{}  (F[k;x]  =  F[k;y]))


By

---

Latex:
(Auto
  THEN  Unfold  `Taylor-approx`  0
  THEN  BLemma  `rsum\_functionality`
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  BLemma  `rmul\_functionality`
  THEN  Auto
  THEN  (BLemma  `rdiv\_functionality`  ORELSE  BLemma  `rnexp\_functionality`)
  THEN  Auto
  THEN  Try  ((BLemma  `rsub\_functionality`\mcdot{}  THEN  Auto)))

---

Home Index