lemma_injective_on_subset

vstd::relations

Function lemma_injective_on_subset 

Source 
pub proof fn lemma_injective_on_subset<X, Y>(
    r: FnSpec<(X,), Y>,
    s1: Set<X>,
    s2: Set<X>,
)
Expand description
requires
s1 <= s2,
injective_on(r, s2),
ensures
injective_on(r, s1),

If a function is injective on a set s2, then it is also injective on any subset s1 of s2.