Function vstd::set_lib::lemma_set_difference_len

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

The length of the set difference A \ B added to the length of the set difference B \ A added to the length of the intersection A ∩ B is equal to the length of the union A + B.

The length of the set difference A \ B is equal to the length of A minus the length of the intersection A ∩ B.