Function vstd::set_lib::lemma_set_union_finite_iff

source · 
pub broadcast proof fn lemma_set_union_finite_iff<A>(s1: Set<A>, s2: Set<A>)
Expand description
ensures
#[trigger] s1.union(s2).finite() <==> s1.finite() && s2.finite(),

The union of two sets is finite iff both sets are finite.