construct_left_inverse

vstd_extra::function_properties

Function construct_left_inverse 

Source 
pub open spec fn construct_left_inverse<A, B>(
    f: FnSpec<(A,), B>,
    domain: Set<A>,
) -> FnSpec<(B,), A>
Expand description
recommends
injective_on(f, domain),
{ |b: B| choose |a: A| domain.contains(a) && f(a) == b }

Constructs a left inverse function g of f when f is injective on domain. For each b in the image, returns the unique a such that f(a) = b.