Commit 2021-09-08 14:01 99b70d9e
View on Github →feat(data/(fin)set/basic): image
and mem
lemmas (#9031)
I rename set.mem_image_of_injective
to function.injective.mem_set_image_iff
to allow dot notation and fit the new function.injective.mem_finset_image_iff
.