Commit 2024-04-24 14:51 c7fa7063

View on Github →

chore: Move intervals (#11765) Move Set.Ixx, Finset.Ixx, Multiset.Ixx together under two different folders:

  • Order.Interval for their definition and basic properties
  • Algebra.Order.Interval for their algebraic properties Move the definitions of Multiset.Ixx to what is now Order.Interval.Multiset. I believe we could just delete this file in a later PR as nothing uses it (and I already had doubts when defining Multiset.Ixx three years ago). Move the algebraic results out of what is now Order.Interval.Finset.Basic to a new file Algebra.Order.Interval.Finset.Basic.

Estimated changes

deleted theorem Finset.image_add_left_Icc
deleted theorem Finset.image_add_left_Ico
deleted theorem Finset.image_add_left_Ioc
deleted theorem Finset.image_add_left_Ioo
deleted theorem Finset.map_add_left_Icc
deleted theorem Finset.map_add_left_Ico
deleted theorem Finset.map_add_left_Ioc
deleted theorem Finset.map_add_left_Ioo
deleted theorem Finset.map_add_right_Icc
deleted theorem Finset.map_add_right_Ico
deleted theorem Finset.map_add_right_Ioc
deleted theorem Finset.map_add_right_Ioo
deleted def Multiset.Icc
deleted def Multiset.Ici
deleted def Multiset.Ico
deleted def Multiset.Iic
deleted def Multiset.Iio
deleted def Multiset.Ioc
deleted def Multiset.Ioi
deleted def Multiset.Ioo
deleted theorem Multiset.mem_Icc
deleted theorem Multiset.mem_Ici
deleted theorem Multiset.mem_Ico
deleted theorem Multiset.mem_Iic
deleted theorem Multiset.mem_Iio
deleted theorem Multiset.mem_Ioc
deleted theorem Multiset.mem_Ioi
deleted theorem Multiset.mem_Ioo
added def Multiset.Icc
added def Multiset.Ici
added def Multiset.Ico
added def Multiset.Iic
added def Multiset.Iio
added def Multiset.Ioc
added def Multiset.Ioi
added def Multiset.Ioo
deleted theorem Multiset.map_add_left_Icc
deleted theorem Multiset.map_add_left_Ico
deleted theorem Multiset.map_add_left_Ioc
deleted theorem Multiset.map_add_left_Ioo
added theorem Multiset.mem_Icc
added theorem Multiset.mem_Ici
added theorem Multiset.mem_Ico
added theorem Multiset.mem_Iic
added theorem Multiset.mem_Iio
added theorem Multiset.mem_Ioc
added theorem Multiset.mem_Ioi
added theorem Multiset.mem_Ioo