Step
*
of Lemma
fps-add_wf
∀[X:Type]. ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)]. ((f+g) ∈ PowerSeries(X;r))
BY
{ (ProveWfLemma THEN Unfold `power-series` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[X:Type]. \mforall{}[r:CRng]. \mforall{}[f,g:PowerSeries(X;r)]. ((f+g) \mmember{} PowerSeries(X;r))
By
Latex:
(ProveWfLemma THEN Unfold `power-series` 0 THEN Auto)
Home
Index