Theorem Function.Embedding.left_inv_of_invOfMemRange

Modification history