Function vstd::multiset::lemma_left_pseudo_idempotence

source ·

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

Expand description

ensures

a.intersection_with(b).intersection_with(b) =~= a.intersection_with(b),

Taking the intersection of multisets a and b and then taking the resulting multiset’s intersection with b again is the same as just taking the intersection of a and b once.