---

Step * 1 of Lemma bag-moebius-property1


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  ∈ ℤ
BY
{ AutoSplit }

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

2
1. T : Type
2. valueall-type(T)
3. eq : EqDecider(T)
4. b : T List
5. ¬(b = {} ∈ bag(T))
⊢ Σ(c∈sub-bags(eq;b)). bag-moebius(eq;c) = 0 ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  valueall-type(T)
3.  eq  :  EqDecider(T)
4.  b  :  T  List
\mvdash{}  \mSigma{}(c\mmember{}sub-bags(eq;b)).  bag-moebius(eq;c)  =  if  bag-null(b)  then  1  else  0  fi 


By

---

Latex:
AutoSplit

---

Home Index