Function vstd::multiset::lemma_multiset_empty_len

source ·

pub proof fn lemma_multiset_empty_len<V>(m: Multiset<V>)

Expand description

ensures

(m.len() == 0 <==> m =~= Multiset::empty())
    && (m.len() > 0 ==> exists |v: V| 0 < m.count(v)),

A multiset is equivalent to the empty multiset if and only if it has length 0. If the multiset has length greater than 0, then there exists some element in the multiset that has a count greater than 0.