right_inverse_on

vstd_extra::function_properties

Function right_inverse_on 

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

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