Theorem Function.Injective.mem_range_iff_existsUnique

Modification history