left_inverse_on

vstd_extra::function_properties

Function left_inverse_on 

Source 
pub open spec fn left_inverse_on<A, B>(
    f: FnSpec<(A,), B>,
    g: FnSpec<(B,), A>,
    domain: Set<A>,
    codomain: Set<B>,
) -> bool
Expand description
{ domain.all(|x: A| codomain.contains(f(x)) && g(f(x)) == x) }

g is a left inverse of f on domain if g(f(x)) == x for all x in domain, and f(x) lies in codomain.