mathlib
99b70d9e - feat(data/(fin)set/basic): `image` and `mem` lemmas (#9031)

Commit
4 years ago
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`.
Author
Parents
Loading