construct_inverse

vstd_extra::function_properties

Function construct_inverse 

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

Constructs the inverse of a bijective function f from domain to codomain. For each b in codomain, returns the unique a in domain such that f(a) == b.