Commit 2023-02-01 14:01 7a4790bb

View on Github →

feat: port Data.Set.Pointwise.Interval (#1481)

  • feat: port Mathlib.Data.Set.Pointwise.Interval
  • Initial file copy from mathport
  • Mathbin -> Mathlib; add import to Mathlib.lean

Estimated changes

added theorem Set.Iic_add_bij
added theorem Set.Iio_add_bij
added theorem Set.image_affine_Icc'
added theorem Set.image_mul_left_Icc
added theorem Set.image_mul_left_Ioo
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.image_neg_uIcc
added theorem Set.inv_Ioi
added theorem Set.inv_Ioo_0_left
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
added theorem Set.preimage_neg_uIcc