---

Step * 1 1 1 of Lemma member-eclass-iff-non-empty


1. T : Type
2. v : bag(T)@i
3. #(v) ≤ 0
4. v ~ {}
⊢ #({}) ∈ ℤ
BY
{ (RepUR ``bag-size empty-bag`` 0 THEN Auto) }

---

Latex:



1.  T  :  Type
2.  v  :  bag(T)@i
3.  \#(v)  \mleq{}  0
4.  v  \msim{}  \{\}
\mvdash{}  \#(\{\})  \mmember{}  \mBbbZ{}


By

(RepUR  ``bag-size  empty-bag``  0  THEN  Auto)

---

Home Index