---

Step * of Lemma sub-bag-iff

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:bag(T).  (sub-bag(T;as;bs) ⇐⇒ ∀x:T. ((#x in as) ≤ (#x in bs)))
BY
{ TACTIC:Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. sub-bag(T;as;bs)
6. x : T
⊢ (#x in as) ≤ (#x in bs)

2
1. [T] : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. ∀x:T. ((#x in as) ≤ (#x in bs))
⊢ sub-bag(T;as;bs)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}as,bs:bag(T).    (sub-bag(T;as;bs)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:T.  ((\#x  in  as)  \mleq{}  (\#x  in  bs)))


By

---

Latex:
TACTIC:Auto

---

Home Index