Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-05 17:51 d9a80ee9

View on Github →

refactor(data/multiset/locally_finite): Generalize multiset.Ico to locally finite orders (#10031) This deletes data.multiset.intervals entirely, redefines multiset.Ico using locally_finite_order and restores the lemmas in their correct generality:

  • multiset.Ico.map_add → multiset.map_add_left_Ico, multiset.map_add_right_Ico
  • multiset.Ico.eq_zero_of_le → multiset.Ico_eq_zero_of_le
  • multiset.Ico.self_eq_zero → multiset.Ico_self
  • multiset.Ico.nodup → multiset.nodup_Ico
  • multiset.Ico.mem → multiset.mem_Ico
  • multiset.Ico.not_mem_top → multiset.right_not_mem_Ico
  • multiset.Ico.inter_consecutive → multiset.Ico_inter_Ico_of_le
  • multiset.Ico.filter_something → multiset.filter_Ico_something
  • multiset.Ico.eq_cons → multiset.Ioo_cons_left
  • multiset.Ico.succ_top →multiset.Ico_cons_right open set multiset now causes a (minor) clash. This explains the changes to analysis.box_integral.divergence_theorem and measure_theory.integral.divergence_theorem

Estimated changes

modified theorem finset.Ico_filter_le_left
deleted theorem multiset.Ico.card
deleted theorem multiset.Ico.eq_cons
deleted theorem multiset.Ico.eq_zero_iff
deleted theorem multiset.Ico.filter_le
deleted theorem multiset.Ico.filter_lt
deleted theorem multiset.Ico.map_add
deleted theorem multiset.Ico.map_sub
deleted theorem multiset.Ico.mem
deleted theorem multiset.Ico.nodup
deleted theorem multiset.Ico.not_mem_top
deleted theorem multiset.Ico.self_eq_zero
deleted theorem multiset.Ico.succ_top
deleted theorem multiset.Ico.zero_bot
deleted def multiset.Ico
added theorem multiset.Ico_filter_le
added theorem multiset.Ico_filter_lt
added theorem multiset.Ico_inter_Ico
added theorem multiset.Ico_self
added theorem multiset.Ioo_cons_left
added theorem multiset.left_mem_Icc
added theorem multiset.left_mem_Ico
added theorem multiset.nodup_Ico
added theorem multiset.right_mem_Icc
added theorem multiset.right_mem_Ioc
modified theorem nat.Icc_succ_left
modified theorem nat.Ico_succ_left
modified theorem nat.Ico_succ_right
modified theorem nat.Ico_succ_singleton
modified theorem nat.Ico_zero_eq_range
modified theorem nat.Iio_eq_range
modified theorem nat.image_sub_const_Ico
added def multiset.Ico
added theorem multiset.mem_Ico
modified theorem set.finite_Icc
modified theorem set.finite_Ico
modified theorem set.finite_Ioc
modified theorem set.finite_Ioo