mathlib
0cf8a98b - chore(data/set): a few more lemmas about `image2` (#4695)

Commit

5 years ago

chore(data/set): a few more lemmas about `image2` (#4695) Also add `@[simp]` to `set.image2_singleton_left` and `set.image2_singleton_rigt`.

References

Author

urkud

Parents