Step
*
of Lemma
Taylor-remainder_wf
∀[I:Interval]. ∀[n:ℕ]. ∀[F:ℕn + 1 ⟶ I ⟶ℝ]. ∀[b,a:{a:ℝ| a ∈ I} ].  (Taylor-remainder(I;n;b;a;i,x.F[i;x]) ∈ ℝ)
BY
{ Using [`I',⌜I⌝] ProveWfLemma⋅ }
Latex:
Latex:
\mforall{}[I:Interval].  \mforall{}[n:\mBbbN{}].  \mforall{}[F:\mBbbN{}n  +  1  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}].  \mforall{}[b,a:\{a:\mBbbR{}|  a  \mmember{}  I\}  ].
    (Taylor-remainder(I;n;b;a;i,x.F[i;x])  \mmember{}  \mBbbR{})
By
Latex:
Using  [`I',\mkleeneopen{}I\mkleeneclose{}]  ProveWfLemma\mcdot{}
Home
Index