Function vstd::set_lib::lemma_set_remove_finite_iff

source · 
pub broadcast proof fn lemma_set_remove_finite_iff<A>(s: Set<A>, a: A)
Expand description
ensures
#[trigger] s.remove(a).finite() <==> s.finite(),

The result of removing an element a into a set s is finite iff s is finite.