---

Step * of Lemma bag-moebius-property

∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[b:bag(T)].
    (bag-moebius(eq;b)
    = if bag-null(b) then 1 else -Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(p)) fi 
    ∈ ℤ) 
  supposing valueall-type(T)
BY
{ (Auto THEN AutoSplit) }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : bag(T)
5. b = {} ∈ bag(T)
⊢ bag-moebius(eq;b) = 1 ∈ ℤ

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : bag(T)
5. ¬(b = {} ∈ bag(T))
⊢ bag-moebius(eq;b) = (-Σ(p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(p))) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[b:bag(T)].
        (bag-moebius(eq;b)
        =  if  bag-null(b)
            then  1
            else  -\mSigma{}(p\mmember{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]).  bag-moebius(eq;snd(p))
            fi  ) 
    supposing  valueall-type(T)


By

---

Latex:
(Auto  THEN  AutoSplit)

---

Home Index