Theorem Function.Injective.right_inv_of_invOfMemRange

Modification history