Function vstd::set_lib::lemma_set_intersect_union_lens

source · 
pub proof fn lemma_set_intersect_union_lens<A>(a: Set<A>, b: Set<A>)
Expand description
requires
a.finite(),
b.finite(),
ensures
(a + b).len() + a.intersect(b).len() == a.len() + b.len(),

The length of the union between two sets added to the length of the intersection between the two sets is equal to the sum of the lengths of the two sets.