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.