mathlib3

d9a80ee9 - refactor(data/multiset/locally_finite): Generalize `multiset.Ico` to locally finite orders (#10031)

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`