lemma_inverse_of_bijection_is_bijective

vstd_extra::function_properties

Function lemma_inverse_of_bijection_is_bijective 

Source 
pub proof fn lemma_inverse_of_bijection_is_bijective<A, B>(
    f: FnSpec<(A,), B>,
    g: FnSpec<(B,), A>,
    domain: Set<A>,
    codomain: Set<B>,
)
Expand description
requires
bijective_on(f, domain, codomain),
left_inverse_on(f, g, domain, codomain) || right_inverse_on(f, g, domain, codomain),
ensures
bijective_on(g, codomain, domain),

If f is a bijection from domain to codomain, and g is either its left or right inverse, then g is a bijection from codomain to domain.