bijective_on

vstd_extra::function_properties

Function bijective_on 

Source 
pub open spec fn bijective_on<A, B>(
    f: FnSpec<(A,), B>,
    domain: Set<A>,
    codomain: Set<B>,
) -> bool
Expand description
{ injective_on(f, domain) && (domain.map(f) =~= codomain) }

A function is bijective from domain to codomain if it is injective on domain and its image equals codomain.