lemma_construct_left_inverse_sound

vstd_extra::function_properties

Function lemma_construct_left_inverse_sound 

Source 
pub proof fn lemma_construct_left_inverse_sound<A, B>(
    f: FnSpec<(A,), B>,
    domain: Set<A>,
)
Expand description
requires
injective_on(f, domain),
ensures
left_inverse_on(f, construct_left_inverse(f, domain), domain, domain.map(f)),

If f is injective on domain, then construct_left_inverse(f, domain) is a left inverse of f on that domain. That is, for all x ∈ domain, we have g(f(x)) == x.