Function lemma_isets_eq_iff_injective_map_on_eq

pub proof fn lemma_isets_eq_iff_injective_map_on_eq<T, S>(
    s1: ISet<T>,
    s2: ISet<T>,
    f: FnSpec<(T,), S>,
)

Expand description

requires

(s1 + s2).injective_on(f),

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.

lemma_isets_eq_iff_injective_map_on_eq