---

Step * of Lemma fps-Pascal-iff

No Annotations
∀[r:CRng]. ∀[x,y:Atom]. ∀[f:PowerSeries(r)].
  fps-Pascal(r;x;y;f) ⇐⇒ f = (((((1-atom(y))*f(x:=0))+((1-atom(x))*f(y:=0)))-f(x:=0)(y:=0))*Δ(x,y)) ∈ PowerSeries(r) 
  supposing ¬(x = y ∈ Atom)
BY
{ ((UnivCD THENA Auto) THEN Unfold `fps-atom` 0) }

1
1. r : CRng
2. x : Atom
3. y : Atom
4. f : PowerSeries(r)
5. ¬(x = y ∈ Atom)
⊢ fps-Pascal(r;x;y;f) ⇐⇒ f = (((((1-<{y}>)*f(x:=0))+((1-<{x}>)*f(y:=0)))-f(x:=0)(y:=0))*Δ(x,y)) ∈ PowerSeries(r)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[r:CRng].  \mforall{}[x,y:Atom].  \mforall{}[f:PowerSeries(r)].
    fps-Pascal(r;x;y;f)
    \mLeftarrow{}{}\mRightarrow{}  f  =  (((((1-atom(y))*f(x:=0))+((1-atom(x))*f(y:=0)))-f(x:=0)(y:=0))*\mDelta{}(x,y)) 
    supposing  \mneg{}(x  =  y)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `fps-atom`  0)

---

Home Index