lemma_bijective_subset_still_bijective

vstd_extra::function_properties

Function lemma_bijective_subset_still_bijective 

Source 
pub proof fn lemma_bijective_subset_still_bijective<A, B>(
    f: FnSpec<(A,), B>,
    domain: Set<A>,
    codomain: Set<B>,
    s: Set<A>,
)
Expand description
requires
bijective_on(f, domain, codomain),
s <= domain,
ensures
bijective_on(f, s, s.map(f)),