Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-25 09:50 e3ae6cd6

View on Github →

feat(data/equiv/basic): lemmas about images and preimages (#6398)

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.eq_preimage_iff_image_eq

added theorem equiv.image_eq_iff_eq

added theorem equiv.image_subset

added theorem equiv.preimage_eq_iff_eq_image

added theorem equiv.preimage_subset

added theorem equiv.preimage_symm_preimage

added theorem equiv.symm_preimage_preimage

Modified src/data/set/basic.lean

added theorem set.eq_preimage_iff_image_eq

added theorem set.preimage_eq_iff_eq_image