---

Step * of Lemma bag-moebius-inversion

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f,g:bag(X) ⟶ |r|].
    ∀b:bag(X). ((g b) = Σ(p∈bag-partitions(eq;b)). (f (fst(p))) * int-to-ring(r;bag-moebius(eq;snd(p))) ∈ |r|) 
    supposing ∀b:bag(X). ((f b) = Σ(s∈sub-bags(eq;b)). g s ∈ |r|) 
  supposing valueall-type(X)
BY
{ xxx(InstLemma `fps-moebius-inversion` []
      THEN Unfold `power-series` -1
      THEN RepeatFor 6 (ParallelLast')
      THEN Auto)xxx }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. f : bag(X) ⟶ |r|
6. g : bag(X) ⟶ |r|
7. g = (f*fps-moebius(eq;r)) ∈ (bag(X) ⟶ |r|) supposing f = (g*λb.1) ∈ (bag(X) ⟶ |r|)
8. ∀b:bag(X). ((f b) = Σ(s∈sub-bags(eq;b)). g s ∈ |r|)
9. b : bag(X)
⊢ (g b) = Σ(p∈bag-partitions(eq;b)). (f (fst(p))) * int-to-ring(r;bag-moebius(eq;snd(p))) ∈ |r|

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f,g:bag(X)  {}\mrightarrow{}  |r|].
        \mforall{}b:bag(X)
            ((g  b)  =  \mSigma{}(p\mmember{}bag-partitions(eq;b)).  (f  (fst(p)))  *  int-to-ring(r;bag-moebius(eq;snd(p)))) 
        supposing  \mforall{}b:bag(X).  ((f  b)  =  \mSigma{}(s\mmember{}sub-bags(eq;b)).  g  s) 
    supposing  valueall-type(X)


By

---

Latex:
xxx(InstLemma  `fps-moebius-inversion`  []
        THEN  Unfold  `power-series`  -1
        THEN  RepeatFor  6  (ParallelLast')
        THEN  Auto)xxx

---

Home Index