---

Step * of Lemma bag-moebius-property1

No Annotations
∀[T:Type]
  ∀[eq:EqDecider(T)]. ∀[b:bag(T)].  (Σ(c∈sub-bags(eq;b)). bag-moebius(eq;c) = if bag-null(b) then 1 else 0 fi  ∈ ℤ) 
  supposing valueall-type(T)
BY
{ (Auto THEN BagToList (-1) THEN Auto THEN Try ((D 0 THEN Reduce 0 THEN Auto))) }

1
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : T List
⊢ Σ(c∈sub-bags(eq;b)). bag-moebius(eq;c) = if bag-null(b) then 1 else 0 fi  ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[b:bag(T)].
        (\mSigma{}(c\mmember{}sub-bags(eq;b)).  bag-moebius(eq;c)  =  if  bag-null(b)  then  1  else  0  fi  ) 
    supposing  valueall-type(T)


By

---

Latex:
(Auto  THEN  BagToList  (-1)  THEN  Auto  THEN  Try  ((D  0  THEN  Reduce  0  THEN  Auto)))

---

Home Index