vstd::set_lib

Function lemma_sets_eq_iff_injective_map_eq

Source 
pub proof fn lemma_sets_eq_iff_injective_map_eq<T, S>(
    s1: Set<T>,
    s2: Set<T>,
    f: FnSpec<(T,), S>,
)
Expand description
requires
super::relations::injective(f),
ensures
(s1 == s2) <==> (s1.map(f) == s2.map(f)),

Two sets are equal iff mapping f results in equal sets, if f is injective.