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.