---

Step * 2 of Lemma mem_bsublist


1. s : DSet
2. as : DisList{s}
3. bs : |s| List
4. ∀c:|s|. ((↑(c ∈b as)) ⇒ (↑(c ∈b bs)))
⊢ ↑bsublist(s;as;bs)
BY
{ ((RWW "mem_iff_count_nzero" 4 THENM RWW "count_bsublist_a" 0) THENA Auto) }

1
1. s : DSet
2. as : DisList{s}
3. bs : |s| List
4. ∀c:|s|. (((c #∈ as) > 0) ⇒ ((c #∈ bs) > 0))
⊢ ∀c:|s|. ((c #∈ as) ≤ (c #∈ bs))

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  DisList\{s\}
3.  bs  :  |s|  List
4.  \mforall{}c:|s|.  ((\muparrow{}(c  \mmember{}\msubb{}  as))  {}\mRightarrow{}  (\muparrow{}(c  \mmember{}\msubb{}  bs)))
\mvdash{}  \muparrow{}bsublist(s;as;bs)


By

---

Latex:
((RWW  "mem\_iff\_count\_nzero"  4  THENM  RWW  "count\_bsublist\_a"  0)  THENA  Auto)

---

Home Index