Theorem Function.Injective.left_inv_of_invOfMemRange

Modification history