Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-09 09:32 94379028

View on Github →

refactor(data/set/pointwise/interval): split (#17873)

  • Extract data.set.interval.monoid from data.set.pointwise.interval.
  • Import it in data.finset.locally_finite, golf some proofs.
  • Add finset.map_add_left_Icc etc.

Estimated changes

modified theorem finset.image_add_left_Icc
modified theorem finset.image_add_left_Ico
modified theorem finset.image_add_left_Ioc
modified theorem finset.image_add_left_Ioo
modified theorem finset.image_add_right_Icc
added theorem set.Icc_add_bij
added theorem set.Ici_add_bij
added theorem set.Ico_add_bij
added theorem set.Ioc_add_bij
added theorem set.Ioi_add_bij
added theorem set.Ioo_add_bij
deleted theorem set.Icc_add_bij
deleted theorem set.Ici_add_bij
deleted theorem set.Ico_add_bij
deleted theorem set.Ioc_add_bij
deleted theorem set.Ioi_add_bij
deleted theorem set.Ioo_add_bij
deleted theorem set.image_add_const_Icc
deleted theorem set.image_add_const_Ici
deleted theorem set.image_add_const_Ico
deleted theorem set.image_add_const_Ioc
deleted theorem set.image_add_const_Ioi
deleted theorem set.image_add_const_Ioo
deleted theorem set.image_const_add_Icc
deleted theorem set.image_const_add_Ici
deleted theorem set.image_const_add_Ico
deleted theorem set.image_const_add_Ioc
deleted theorem set.image_const_add_Ioi
deleted theorem set.image_const_add_Ioo