---

Step * of Lemma bag-member-iff-size

∀[T:Type]. ∀[bs:bag(T)].  uiff(↓∃x:T. x ↓∈ bs;0 < #(bs))
BY
{ Auto }

1
1. T : Type
2. bs : bag(T)
3. ∃x:T. x ↓∈ bs
⊢ 0 < #(bs)

2
1. T : Type
2. bs : bag(T)
3. 0 < #(bs)
⊢ ↓∃x:T. x ↓∈ bs

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[bs:bag(T)].    uiff(\mdownarrow{}\mexists{}x:T.  x  \mdownarrow{}\mmember{}  bs;0  <  \#(bs))


By

---

Latex:
Auto

---

Home Index