Function vstd::set_lib::lemma_set_disjoint

source ·

pub proof fn lemma_set_disjoint<A>(a: Set<A>, b: Set<A>)

Expand description

ensures

a.disjoint(b) ==> ((a + b).difference(a) =~= b && (a + b).difference(b) =~= a),

If sets a and b are disjoint, meaning they have no elements in common, then the set difference of a + b and b is equal to a and the set difference of a + b and a is equal to b.