set.maps_to

maps_to f a b means that the image of a is contained in b.

set.inj_on

f is injective on a if the restriction of f to a is injective.

set.surj_on

f is surjective from a to b if b is contained in the image of a.

set.bij_on

f is bijective from a to b if f is injective on a and f '' a = b.

set.left_inv_on

g is a left inverse to f on a means that g (f x) = x for all x ∈ a.

set.right_inv_on

g is a right inverse to f on b if f (g x) = x for all x ∈ b.

set.inv_on

g is an inverse to f viewed as a map from a to b