---

Step * of Lemma non-empty-bag-union-of-list

∀[T:Type]. ∀L:bag(T) List. (0 < #(bag-union(L)) ⇐⇒ (∃b∈L. 0 < #(b)))
BY
{ InductionOnList }

1
1. [T] : Type
⊢ 0 < #(bag-union([])) ⇐⇒ (∃b∈[]. 0 < #(b))

2
1. [T] : Type
2. u : bag(T)
3. v : bag(T) List
4. 0 < #(bag-union(v)) ⇐⇒ (∃b∈v. 0 < #(b))
⊢ 0 < #(bag-union([u / v])) ⇐⇒ (∃b∈[u / v]. 0 < #(b))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:bag(T)  List.  (0  <  \#(bag-union(L))  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}b\mmember{}L.  0  <  \#(b)))


By

---

Latex:
InductionOnList

---

Home Index