lemma_two_sided_inverse_implies_bijective

vstd_extra::function_properties

Function lemma_two_sided_inverse_implies_bijective 

Source 
pub proof fn lemma_two_sided_inverse_implies_bijective<A, B>(
    f: FnSpec<(A,), B>,
    g: FnSpec<(B,), A>,
    domain: Set<A>,
    codomain: Set<B>,
)
Expand description
requires
inverse_on(f, g, domain, codomain),
ensures
bijective_on(f, domain, codomain),

If f has a two-sided inverse g on domain and codomain, then f is bijective on that domain and codomain.