---

Step * of Lemma mem_bsubmset

∀s:DSet. ∀a:FiniteSet{s}. ∀b:MSet{s}.  (↑(a ⊆b b) ⇐⇒ ∀x:|s|. ((↑(x ∈b a)) ⇒ (↑(x ∈b b))))
BY
{ ((RepD THENM RewriteWith [] 
  ``count_bsubmset mset_mem_iff_count_nzero`` 0) THENA Auto) }

1
1. s : DSet@i'
2. a : FiniteSet{s}@i
3. b : MSet{s}@i
⊢ ∀x:|s|. ((x #∈ a) ≤ (x #∈ b)) ⇐⇒ ∀x:|s|. (((x #∈ a) > 0) ⇒ ((x #∈ b) > 0))

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:FiniteSet\{s\}.  \mforall{}b:MSet\{s\}.    (\muparrow{}(a  \msubseteq{}\msubb{}  b)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  a))  {}\mRightarrow{}  (\muparrow{}(x  \mmember{}\msubb{}  b))))


By

---

Latex:
((RepD  THENM  RewriteWith  [] 
    ``count\_bsubmset  mset\_mem\_iff\_count\_nzero``  0)  THENA  Auto)

---

Home Index