Function vstd::set_lib::lemma_set_empty_equivalency_len

source · 
pub proof fn lemma_set_empty_equivalency_len<A>(s: Set<A>)
Expand description
requires
s.finite(),
ensures
(s.len() == 0 <==> s == Set::<A>::empty())
    && (s.len() != 0 ==> exists |x: A| s.contains(x)),

Set s has length 0 if and only if it is equal to the empty set. If s has length greater than 0, Then there must exist an element x such that s contains x.