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