Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-05 10:41 fd623d6c

View on Github →

feat(data/set/intervals/image_preimage): new file (#2958)

  • Create a file for lemmas like (λ x, x + a) '' Icc b c = Icc (b + a) (b + c).
  • Prove lemmas about images and preimages of all intervals under x ↦ x ± a, x ↦ a ± x, and x ↦ -x.
  • Move lemmas about multiplication from basic.

Estimated changes

deleted theorem set.image_add_left_Icc
deleted theorem set.image_add_right_Icc
deleted theorem set.image_mul_left_Icc'
deleted theorem set.image_mul_left_Icc
deleted theorem set.image_mul_right_Icc'
deleted theorem set.image_mul_right_Icc
deleted theorem set.image_neg_Iic
deleted theorem set.image_neg_Iio
added theorem set.image_mul_left_Icc
added theorem set.image_neg_Icc
added theorem set.image_neg_Ici
added theorem set.image_neg_Ico
added theorem set.image_neg_Iic
added theorem set.image_neg_Iio
added theorem set.image_neg_Ioc
added theorem set.image_neg_Ioi
added theorem set.image_neg_Ioo
added theorem set.preimage_neg_Icc
added theorem set.preimage_neg_Ici
added theorem set.preimage_neg_Ico
added theorem set.preimage_neg_Iic
added theorem set.preimage_neg_Iio
added theorem set.preimage_neg_Ioc
added theorem set.preimage_neg_Ioi
added theorem set.preimage_neg_Ioo