Step
*
of Lemma
mem_lmin
∀s:DSet. ∀as,bs:|s| List. ∀c:|s|. c ∈b lmin(s;as;bs) = (c ∈b as) ∧b (c ∈b bs)
BY
{ ((((RepD THENM BLemma `iff_imp_equal_bool`) THENM RW bool_to_propC 0) THENM RWH (LemmaC `mem_iff_count_nzero`) 0)
THENA Auto
) }
1
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. c : |s|
⊢ (c #∈ lmin(s;as;bs)) > 0
⇐⇒ ((c #∈ as) > 0) ∧ ((c #∈ bs) > 0)
Latex:
Latex:
\mforall{}s:DSet. \mforall{}as,bs:|s| List. \mforall{}c:|s|. c \mmember{}\msubb{} lmin(s;as;bs) = (c \mmember{}\msubb{} as) \mwedge{}\msubb{} (c \mmember{}\msubb{} bs)
By
Latex:
((((RepD THENM BLemma `iff\_imp\_equal\_bool`) THENM RW bool\_to\_propC 0)
THENM RWH (LemmaC `mem\_iff\_count\_nzero`) 0
)
THENA Auto
)
Home
Index