lemma_construct_inverse_sound

vstd_extra::function_properties

Function lemma_construct_inverse_sound 

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

If f is bijective from domain to codomain, then construct_inverse(f, domain, codomain) is a two-sided inverse of f on that domain and codomain. That is, for all x ∈ domain, we have g(f(x)) == x and for all y ∈ codomain, we have f(g(y)) == y.