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`

src/data/finset/locally_finite.lean

@@ -78,31 +78,31 @@ lemma right_mem_Ioc : b ∈ Ioc a b ↔ a < b := by simp only [mem_Ioc, and_true
 @[simp] lemma right_not_mem_Ico : b ∉ Ico a b := λ h, lt_irrefl _ (mem_Ico.1 h).2
 @[simp] lemma right_not_mem_Ioo : b ∉ Ioo a b := λ h, lt_irrefl _ (mem_Ioo.1 h).2
 
-lemma Ico_filter_lt_of_le_left [decidable_rel ((<) : α → α → Prop)] {a b c : α} (hca : c ≤ a) :
+lemma Ico_filter_lt_of_le_left {a b c : α} [decidable_pred (< c)] (hca : c ≤ a) :
   (Ico a b).filter (λ x, x < c) = ∅ :=
 finset.filter_false_of_mem (λ x hx, (hca.trans (mem_Ico.1 hx).1).not_lt)
 
-lemma Ico_filter_lt_of_right_le [decidable_rel ((<) : α → α → Prop)] {a b c : α} (hbc : b ≤ c) :
+lemma Ico_filter_lt_of_right_le {a b c : α} [decidable_pred (< c)] (hbc : b ≤ c) :
   (Ico a b).filter (λ x, x < c) = Ico a b :=
 finset.filter_true_of_mem (λ x hx, (mem_Ico.1 hx).2.trans_le hbc)
 
-lemma Ico_filter_lt_of_le_right [decidable_rel ((<) : α → α → Prop)] {a b c : α} (hcb : c ≤ b) :
+lemma Ico_filter_lt_of_le_right {a b c : α} [decidable_pred (< c)] (hcb : c ≤ b) :
   (Ico a b).filter (λ x, x < c) = Ico a c :=
 begin
   ext x,
   rw [mem_filter, mem_Ico, mem_Ico, and.right_comm],
   exact and_iff_left_of_imp (λ h, h.2.trans_le hcb),
 end
 
-lemma Ico_filter_le_of_le_left [decidable_rel ((≤) : α → α → Prop)] {a b c : α} (hca : c ≤ a) :
+lemma Ico_filter_le_of_le_left {a b c : α} [decidable_pred ((≤) c)] (hca : c ≤ a) :
   (Ico a b).filter (λ x, c ≤ x) = Ico a b :=
 finset.filter_true_of_mem (λ x hx, hca.trans (mem_Ico.1 hx).1)
 
-lemma Ico_filter_le_of_right_le [decidable_rel ((≤) : α → α → Prop)] {a b : α} :
+lemma Ico_filter_le_of_right_le {a b : α} [decidable_pred ((≤) b)] :
   (Ico a b).filter (λ x, b ≤ x) = ∅ :=
 finset.filter_false_of_mem (λ x hx, (mem_Ico.1 hx).2.not_le)
 
-lemma Ico_filter_le_of_left_le [decidable_rel ((≤) : α → α → Prop)] {a b c : α} (hac : a ≤ c) :
+lemma Ico_filter_le_of_left_le {a b c : α} [decidable_pred ((≤) c)] (hac : a ≤ c) :
   (Ico a b).filter (λ x, c ≤ x) = Ico c b :=
 begin
   ext x,
@@ -153,7 +153,7 @@ le_of_eq $ Ico_inter_Ico_consecutive a b c
 
 end decidable_eq
 
-lemma Ico_filter_le_left [decidable_rel ((≤) : α → α → Prop)] {a b : α} (hab : a < b) :
+lemma Ico_filter_le_left {a b : α} [decidable_pred (≤ a)] (hab : a < b) :
   (Ico a b).filter (λ x, x ≤ a) = {a} :=
 begin
   ext x,

src/data/multiset/default.lean

@@ -4,8 +4,8 @@ import data.multiset.erase_dup
 import data.multiset.finset_ops
 import data.multiset.fold
 import data.multiset.functor
-import data.multiset.intervals
 import data.multiset.lattice
+import data.multiset.locally_finite
 import data.multiset.nat_antidiagonal
 import data.multiset.nodup
 import data.multiset.pi

src/data/multiset/locally_finite.lean

@@ -10,62 +10,153 @@ import data.finset.locally_finite
 
 This file provides basic results about all the `multiset.Ixx`, which are defined in
 `order.locally_finite`.
-
-## TODO
-
-Bring the lemmas about `multiset.Ico` in `data.multiset.intervals` here and in `data.nat.interval`.
 -/
 
 variables {α : Type*}
 
 namespace multiset
 section preorder
-variables [preorder α] [locally_finite_order α] {a b : α}
+variables [preorder α] [locally_finite_order α] {a b c : α}
 
 lemma nodup_Icc : (Icc a b).nodup := finset.nodup _
+lemma nodup_Ico : (Ico a b).nodup := finset.nodup _
 lemma nodup_Ioc : (Ioc a b).nodup := finset.nodup _
 lemma nodup_Ioo : (Ioo a b).nodup := finset.nodup _
 
 @[simp] lemma Icc_eq_zero_iff : Icc a b = 0 ↔ ¬a ≤ b :=
 by rw [Icc, finset.val_eq_zero, finset.Icc_eq_empty_iff]
 
+@[simp] lemma Ico_eq_zero_iff : Ico a b = 0 ↔ ¬a < b :=
+by rw [Ico, finset.val_eq_zero, finset.Ico_eq_empty_iff]
+
 @[simp] lemma Ioc_eq_zero_iff : Ioc a b = 0 ↔ ¬a < b :=
 by rw [Ioc, finset.val_eq_zero, finset.Ioc_eq_empty_iff]
 
 @[simp] lemma Ioo_eq_zero_iff [densely_ordered α] : Ioo a b = 0 ↔ ¬a < b :=
 by rw [Ioo, finset.val_eq_zero, finset.Ioo_eq_empty_iff]
 
 alias Icc_eq_zero_iff ↔ _ multiset.Icc_eq_zero
+alias Ico_eq_zero_iff ↔ _ multiset.Ico_eq_zero
 alias Ioc_eq_zero_iff ↔ _ multiset.Ioc_eq_zero
 
 @[simp] lemma Ioo_eq_zero (h : ¬a < b) : Ioo a b = 0 :=
 eq_zero_iff_forall_not_mem.2 $ λ x hx, h ((mem_Ioo.1 hx).1.trans (mem_Ioo.1 hx).2)
 
 @[simp] lemma Icc_eq_zero_of_lt (h : b < a) : Icc a b = 0 := Icc_eq_zero h.not_le
+@[simp] lemma Ico_eq_zero_of_le (h : b ≤ a) : Ico a b = 0 := Ico_eq_zero h.not_lt
 @[simp] lemma Ioc_eq_zero_of_le (h : b ≤ a) : Ioc a b = 0 := Ioc_eq_zero h.not_lt
 @[simp] lemma Ioo_eq_zero_of_le (h : b ≤ a) : Ioo a b = 0 := Ioo_eq_zero h.not_lt
 
 variables (a)
 
+@[simp] lemma Ico_self : Ico a a = 0 := by rw [Ico, finset.Ico_self, finset.empty_val]
 @[simp] lemma Ioc_self : Ioc a a = 0 := by rw [Ioc, finset.Ioc_self, finset.empty_val]
 @[simp] lemma Ioo_self : Ioo a a = 0 := by rw [Ioo, finset.Ioo_self, finset.empty_val]
 
+variables {a b c}
+
+lemma left_mem_Icc : a ∈ Icc a b ↔ a ≤ b := finset.left_mem_Icc
+lemma left_mem_Ico : a ∈ Ico a b ↔ a < b := finset.left_mem_Ico
+lemma right_mem_Icc : b ∈ Icc a b ↔ a ≤ b := finset.right_mem_Icc
+lemma right_mem_Ioc : b ∈ Ioc a b ↔ a < b := finset.right_mem_Ioc
+
+@[simp] lemma left_not_mem_Ioc : a ∉ Ioc a b := finset.left_not_mem_Ioc
+@[simp] lemma left_not_mem_Ioo : a ∉ Ioo a b := finset.left_not_mem_Ioo
+@[simp] lemma right_not_mem_Ico : b ∉ Ico a b := finset.right_not_mem_Ico
+@[simp] lemma right_not_mem_Ioo : b ∉ Ioo a b := finset.right_not_mem_Ioo
+
+lemma Ico_filter_lt_of_le_left [decidable_pred (< c)] (hca : c ≤ a) :
+  (Ico a b).filter (λ x, x < c) = ∅ :=
+by { rw [Ico, ←finset.filter_val, finset.Ico_filter_lt_of_le_left hca], refl }
+
+lemma Ico_filter_lt_of_right_le [decidable_pred (< c)] (hbc : b ≤ c) :
+  (Ico a b).filter (λ x, x < c) = Ico a b :=
+by rw [Ico, ←finset.filter_val, finset.Ico_filter_lt_of_right_le hbc]
+
+lemma Ico_filter_lt_of_le_right [decidable_pred (< c)] (hcb : c ≤ b) :
+  (Ico a b).filter (λ x, x < c) = Ico a c :=
+by { rw [Ico, ←finset.filter_val, finset.Ico_filter_lt_of_le_right hcb], refl }
+
+lemma Ico_filter_le_of_le_left [decidable_pred ((≤) c)] (hca : c ≤ a) :
+  (Ico a b).filter (λ x, c ≤ x) = Ico a b :=
+by rw [Ico, ←finset.filter_val, finset.Ico_filter_le_of_le_left hca]
+
+lemma Ico_filter_le_of_right_le [decidable_pred ((≤) b)] :
+  (Ico a b).filter (λ x, b ≤ x) = ∅ :=
+by { rw [Ico, ←finset.filter_val, finset.Ico_filter_le_of_right_le], refl }
+
+lemma Ico_filter_le_of_left_le [decidable_pred ((≤) c)] (hac : a ≤ c) :
+  (Ico a b).filter (λ x, c ≤ x) = Ico c b :=
+by { rw [Ico, ←finset.filter_val, finset.Ico_filter_le_of_left_le hac], refl }
+
 end preorder
 
 section partial_order
 variables [partial_order α] [locally_finite_order α] {a b : α}
 
 @[simp] lemma Icc_self (a : α) : Icc a a = {a} := by rw [Icc, finset.Icc_self, finset.singleton_val]
 
+lemma Ico_cons_right (h : a ≤ b) : b ::ₘ (Ico a b) = Icc a b :=
+by { classical,
+  rw [Ico, ←finset.insert_val_of_not_mem right_not_mem_Ico, finset.Ico_insert_right h], refl }
+
+lemma Ioo_cons_left (h : a < b) : a ::ₘ (Ioo a b) = Ico a b :=
+by { classical,
+  rw [Ioo, ←finset.insert_val_of_not_mem left_not_mem_Ioo, finset.Ioo_insert_left h], refl }
+
+lemma Ico_disjoint_Ico {a b c d : α} (h : b ≤ c) : (Ico a b).disjoint (Ico c d) :=
+λ x hab hbc, by { rw mem_Ico at hab hbc, exact hab.2.not_le (h.trans hbc.1) }
+
+@[simp] lemma Ico_inter_Ico_of_le [decidable_eq α] {a b c d : α} (h : b ≤ c) :
+  Ico a b ∩ Ico c d = 0 :=
+multiset.inter_eq_zero_iff_disjoint.2 $ Ico_disjoint_Ico h
+
+lemma Ico_filter_le_left {a b : α} [decidable_pred (≤ a)] (hab : a < b) :
+  (Ico a b).filter (λ x, x ≤ a) = {a} :=
+by { rw [Ico, ←finset.filter_val, finset.Ico_filter_le_left hab], refl }
+
 end partial_order
 
+section linear_order
+variables [linear_order α] [locally_finite_order α] {a b c d : α}
+
+lemma Ico_subset_Ico_iff {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
+  Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
+finset.Ico_subset_Ico_iff h
+
+lemma Ico_add_Ico_eq_Ico {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
+  Ico a b + Ico b c = Ico a c :=
+by rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ←finset.union_val,
+  finset.Ico_union_Ico_eq_Ico hab hbc]
+
+lemma Ico_inter_Ico : Ico a b ∩ Ico c d = Ico (max a c) (min b d) :=
+by rw [Ico, Ico, Ico, ←finset.inter_val, finset.Ico_inter_Ico]
+
+@[simp] lemma Ico_filter_lt (a b c : α) : (Ico a b).filter (λ x, x < c) = Ico a (min b c) :=
+by rw [Ico, Ico, ←finset.filter_val, finset.Ico_filter_lt]
+
+@[simp] lemma Ico_filter_le (a b c : α) : (Ico a b).filter (λ x, c ≤ x) = Ico (max a c) b :=
+by rw [Ico, Ico, ←finset.filter_val, finset.Ico_filter_le]
+
+@[simp] lemma Ico_sub_Ico_left (a b c : α) : Ico a b - Ico a c = Ico (max a c) b :=
+by rw [Ico, Ico, Ico, ←finset.sdiff_val, finset.Ico_diff_Ico_left]
+
+@[simp] lemma Ico_sub_Ico_right (a b c : α) : Ico a b - Ico c b = Ico a (min b c) :=
+by rw [Ico, Ico, Ico, ←finset.sdiff_val, finset.Ico_diff_Ico_right]
+
+end linear_order
+
 section ordered_cancel_add_comm_monoid
 variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] [locally_finite_order α]
 
 lemma map_add_left_Icc (a b c : α) : (Icc a b).map ((+) c) = Icc (c + a) (c + b) :=
 by { classical, rw [Icc, Icc, ←finset.image_add_left_Icc, finset.image_val,
     (multiset.nodup_map (add_right_injective c) $ finset.nodup _).erase_dup] }
 
+lemma map_add_left_Ico (a b c : α) : (Ico a b).map ((+) c) = Ico (c + a) (c + b) :=
+by { classical, rw [Ico, Ico, ←finset.image_add_left_Ico, finset.image_val,
+    (multiset.nodup_map (add_right_injective c) $ finset.nodup _).erase_dup] }
+
 lemma map_add_left_Ioc (a b c : α) : (Ioc a b).map ((+) c) = Ioc (c + a) (c + b) :=
 by { classical, rw [Ioc, Ioc, ←finset.image_add_left_Ioc, finset.image_val,
     (multiset.nodup_map (add_right_injective c) $ finset.nodup _).erase_dup] }
@@ -77,6 +168,9 @@ by { classical, rw [Ioo, Ioo, ←finset.image_add_left_Ioo, finset.image_val,
 lemma map_add_right_Icc (a b c : α) : (Icc a b).map (λ x, x + c) = Icc (a + c) (b + c) :=
 by { simp_rw add_comm _ c, exact map_add_left_Icc _ _ _ }
 
+lemma map_add_right_Ico (a b c : α) : (Ico a b).map (λ x, x + c) = Ico (a + c) (b + c) :=
+by { simp_rw add_comm _ c, exact map_add_left_Ico _ _ _ }
+
 lemma map_add_right_Ioc (a b c : α) : (Ioc a b).map (λ x, x + c) = Ioc (a + c) (b + c) :=
 by { simp_rw add_comm _ c, exact map_add_left_Ioc _ _ _ }
 

src/data/nat/interval.lean

@@ -62,11 +62,9 @@ lemma Ico_eq_range' : Ico a b = (list.range' a (b - a)).to_finset := rfl
 lemma Ioc_eq_range' : Ioc a b = (list.range' (a + 1) (b - a)).to_finset := rfl
 lemma Ioo_eq_range' : Ioo a b = (list.range' (a + 1) (b - a - 1)).to_finset := rfl
 
-lemma Iio_eq_range : Iio = range :=
-by { ext b x, rw [mem_Iio, mem_range] }
+lemma Iio_eq_range : Iio = range := by { ext b x, rw [mem_Iio, mem_range] }
 
-lemma Ico_zero_eq_range : Ico 0 a = range a :=
-by rw [←bot_eq_zero, ←Iio_eq_Ico, Iio_eq_range]
+lemma Ico_zero_eq_range : Ico 0 a = range a := by rw [←bot_eq_zero, ←Iio_eq_Ico, Iio_eq_range]
 
 lemma _root_.finset.range_eq_Ico : range = Ico 0 := by { funext, exact (Ico_zero_eq_range n).symm }
 
@@ -105,23 +103,19 @@ by rw [fintype.card_of_finset, card_Iio]
 
 -- TODO@Yaël: Generalize all the following lemmas to `succ_order`
 
-lemma Icc_succ_left : Icc a.succ b = Ioc a b :=
-by { ext x, rw [mem_Icc, mem_Ioc, succ_le_iff] }
+lemma Icc_succ_left : Icc a.succ b = Ioc a b := by { ext x, rw [mem_Icc, mem_Ioc, succ_le_iff] }
 
-lemma Ico_succ_right : Ico a b.succ = Icc a b :=
-by { ext x, rw [mem_Ico, mem_Icc, lt_succ_iff] }
+lemma Ico_succ_right : Ico a b.succ = Icc a b := by { ext x, rw [mem_Ico, mem_Icc, lt_succ_iff] }
 
-lemma Ico_succ_left : Ico a.succ b = Ioo a b :=
-by { ext x, rw [mem_Ico, mem_Ioo, succ_le_iff] }
+lemma Ico_succ_left : Ico a.succ b = Ioo a b := by { ext x, rw [mem_Ico, mem_Ioo, succ_le_iff] }
 
 lemma Icc_pred_right {b : ℕ} (h : 0 < b) : Icc a (b - 1) = Ico a b :=
 by { ext x, rw [mem_Icc, mem_Ico, lt_iff_le_pred h] }
 
 lemma Ico_succ_succ : Ico a.succ b.succ = Ioc a b :=
 by { ext x, rw [mem_Ico, mem_Ioc, succ_le_iff, lt_succ_iff] }
 
-@[simp] lemma Ico_succ_singleton : Ico a (a + 1) = {a} :=
-by rw [Ico_succ_right, Icc_self]
+@[simp] lemma Ico_succ_singleton : Ico a (a + 1) = {a} := by rw [Ico_succ_right, Icc_self]
 
 @[simp] lemma Ico_pred_singleton {a : ℕ} (h : 0 < a) : Ico (a - 1) a = {a - 1} :=
 by rw [←Icc_pred_right _ h, Icc_self]
@@ -134,8 +128,7 @@ by rw [Ico_succ_right, ←Ico_insert_right h]
 lemma Ico_insert_succ_left (h : a < b) : insert a (Ico a.succ b) = Ico a b :=
 by rw [Ico_succ_left, ←Ioo_insert_left h]
 
-lemma image_sub_const_Ico (h : c ≤ a) :
-  (Ico a b).image (λ x, x - c) = Ico (a - c) (b - c) :=
+lemma image_sub_const_Ico (h : c ≤ a) : (Ico a b).image (λ x, x - c) = Ico (a - c) (b - c) :=
 begin
   ext x,
   rw mem_image,
@@ -173,8 +166,7 @@ begin
         tsub_le_iff_right.1 hb⟩ } }
 end
 
-lemma range_image_pred_top_sub (n : ℕ) :
-  (finset.range n).image (λ j, n - 1 - j) = finset.range n :=
+lemma range_image_pred_top_sub (n : ℕ) : (finset.range n).image (λ j, n - 1 - j) = finset.range n :=
 begin
   cases n,
   { rw [range_zero, image_empty] },