Function vstd::set_lib::lemma_map_size

source · 
pub proof fn lemma_map_size<A, B>(x: Set<A>, y: Set<B>, f: FnSpec<(A,), B>)
Expand description
requires
injective(f),
forall |a: A| x.contains(a) ==> y.contains(#[trigger] f(a)),
forall |b: B| (#[trigger] y.contains(b)) ==> exists |a: A| x.contains(a) && f(a) == b,
x.finite(),
y.finite(),
ensures
x.len() == y.len(),

If an injective function is applied to each element of a set to construct another set, the two sets have the same size.