lemma_sets_eq_iff_injective_map_on_eq

vstd::set_lib

Function lemma_sets_eq_iff_injective_map_on_eq 

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

Two sets are equal iff applying an injective (in the union of the sets) function f to each set produces equal sets.