Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-21 23:51 9ec2778f

View on Github →

chore(data/{equiv,set}/basic): image_preimage (#5465)

  • equiv.symm_image_image: add @[simp];
  • equiv.image_preimage, equiv.preimage_image: new simp lemmas;
  • set.image_preimage_eq, set.preimage_image_eq: make s : set _ an explicit argument;
  • function.injective.preimage_image, function.surjective.image_preimage: new aliases for set.preimage_image_eq and set.image_preimage_eq with arguments reversed Also golf a proof about separated.

Estimated changes

added theorem equiv.image_preimage
added theorem equiv.preimage_image
modified theorem equiv.symm_image_image
modified theorem set.image_preimage_eq
modified theorem set.preimage_eq_preimage