Function vstd::multiset::lemma_intersection_count

pub proof fn lemma_intersection_count<V>(a: Multiset<V>, b: Multiset<V>, x: V)

Expand description

ensures

a.intersection_with(b).count(x) == min(a.count(x) as int, b.count(x) as int),

The multiplicity of an element x in the intersection of multisets a and b will be the minimum count of x in either a or b.

Function vstd::multiset::lemma_intersection_countCopy item path