Skip to main content

lemma_iset_disjoint_iff_empty_intersection

Function lemma_iset_disjoint_iff_empty_intersection 

Source
pub proof fn lemma_iset_disjoint_iff_empty_intersection<T>(a: ISet<T>, b: ISet<T>)
Expand description
ensures
a.disjoint(b) <==> a.intersect(b).is_empty(),

Two sets are disjoint iff their intersection is empty