---

Step * 1 of Lemma assert-member-eclass


1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. e : E
6. v : bag(T)@i
7. (X es e) = v ∈ bag(T)@i
⊢ ¬(#(v) = 0 ∈ ℤ) ⇐⇒ ↓∃v@0:T. v@0 ↓∈ v
BY
{ (InstLemma `bag-member-iff-size` [⌈T⌉;⌈v⌉]⋅ THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  es  :  EO+(Info)
5.  e  :  E
6.  v  :  bag(T)@i
7.  (X  es  e)  =  v@i
\mvdash{}  \mneg{}(\#(v)  =  0)  \mLeftarrow{}{}\mRightarrow{}  \mdownarrow{}\mexists{}v@0:T.  v@0  \mdownarrow{}\mmember{}  v


By

(InstLemma  `bag-member-iff-size`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index