From d9a80ee9c79b71d8ad0e9dc9fd3140abf38b3358 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Fri, 5 Nov 2021 17:51:17 +0000 Subject: [PATCH] refactor(data/multiset/locally_finite): Generalize `multiset.Ico` to locally finite orders (#10031) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 14 ++-- src/data/multiset/default.lean | 2 +- src/data/multiset/intervals.lean | 101 ------------------------- src/data/multiset/locally_finite.lean | 104 ++++++++++++++++++++++++-- src/data/nat/interval.lean | 24 ++---- src/order/locally_finite.lean | 38 ++++------ 6 files changed, 129 insertions(+), 154 deletions(-) delete mode 100644 src/data/multiset/intervals.lean diff --git a/src/data/finset/locally_finite.lean b/src/data/finset/locally_finite.lean index 10822a07125c9..dfc91aa831ea4 100644 --- a/src/data/finset/locally_finite.lean +++ b/src/data/finset/locally_finite.lean @@ -78,15 +78,15 @@ 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, @@ -94,15 +94,15 @@ begin 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, diff --git a/src/data/multiset/default.lean b/src/data/multiset/default.lean index 965e0313a2ee3..e341db806bcd2 100644 --- a/src/data/multiset/default.lean +++ b/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 diff --git a/src/data/multiset/intervals.lean b/src/data/multiset/intervals.lean deleted file mode 100644 index 8e88e9c9630dd..0000000000000 --- a/src/data/multiset/intervals.lean +++ /dev/null @@ -1,101 +0,0 @@ -/- -Copyright (c) 2019 Scott Morrison. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison --/ -import data.multiset.nodup -import data.list.intervals - -/-! -# Intervals in ℕ as multisets - -For now this only covers `Ico n m`, the "closed-open" interval containing `[n, ..., m-1]`. --/ - -namespace multiset -open list - -/-! ### Ico -/ - -/-- `Ico n m` is the multiset lifted from the list `Ico n m`, e.g. the set `{n, n+1, ..., m-1}`. -/ -def Ico (n m : ℕ) : multiset ℕ := Ico n m - -namespace Ico - -theorem map_add (n m k : ℕ) : (Ico n m).map ((+) k) = Ico (n + k) (m + k) := -congr_arg coe $ list.Ico.map_add _ _ _ - -theorem map_sub (n m k : ℕ) (h : k ≤ n) : (Ico n m).map (λ x, x - k) = Ico (n - k) (m - k) := -congr_arg coe $ list.Ico.map_sub _ _ _ h - -theorem zero_bot (n : ℕ) : Ico 0 n = range n := -congr_arg coe $ list.Ico.zero_bot _ - -@[simp] theorem card (n m : ℕ) : (Ico n m).card = m - n := -list.Ico.length _ _ - -theorem nodup (n m : ℕ) : nodup (Ico n m) := Ico.nodup _ _ - -@[simp] theorem mem {n m l : ℕ} : l ∈ Ico n m ↔ n ≤ l ∧ l < m := -list.Ico.mem - -theorem eq_zero_of_le {n m : ℕ} (h : m ≤ n) : Ico n m = 0 := -congr_arg coe $ list.Ico.eq_nil_of_le h - -@[simp] theorem self_eq_zero {n : ℕ} : Ico n n = 0 := -eq_zero_of_le $ le_refl n - -@[simp] theorem eq_zero_iff {n m : ℕ} : Ico n m = 0 ↔ m ≤ n := -iff.trans (coe_eq_zero _) list.Ico.eq_empty_iff - -lemma add_consecutive {n m l : ℕ} (hnm : n ≤ m) (hml : m ≤ l) : - Ico n m + Ico m l = Ico n l := -congr_arg coe $ list.Ico.append_consecutive hnm hml - -@[simp] lemma inter_consecutive (n m l : ℕ) : Ico n m ∩ Ico m l = 0 := -congr_arg coe $ list.Ico.bag_inter_consecutive n m l - -@[simp] theorem succ_singleton {n : ℕ} : Ico n (n+1) = {n} := -congr_arg coe $ list.Ico.succ_singleton - -theorem succ_top {n m : ℕ} (h : n ≤ m) : Ico n (m + 1) = m ::ₘ Ico n m := -by rw [Ico, list.Ico.succ_top h, ← coe_add, add_comm]; refl - -theorem eq_cons {n m : ℕ} (h : n < m) : Ico n m = n ::ₘ Ico (n + 1) m := -congr_arg coe $ list.Ico.eq_cons h - -@[simp] theorem pred_singleton {m : ℕ} (h : 0 < m) : Ico (m - 1) m = {m - 1} := -congr_arg coe $ list.Ico.pred_singleton h - -@[simp] theorem not_mem_top {n m : ℕ} : m ∉ Ico n m := -list.Ico.not_mem_top - -lemma filter_lt_of_top_le {n m l : ℕ} (hml : m ≤ l) : (Ico n m).filter (λ x, x < l) = Ico n m := -congr_arg coe $ list.Ico.filter_lt_of_top_le hml - -lemma filter_lt_of_le_bot {n m l : ℕ} (hln : l ≤ n) : (Ico n m).filter (λ x, x < l) = ∅ := -congr_arg coe $ list.Ico.filter_lt_of_le_bot hln - -lemma filter_le_of_bot {n m : ℕ} (hnm : n < m) : (Ico n m).filter (λ x, x ≤ n) = {n} := -congr_arg coe $ list.Ico.filter_le_of_bot hnm - -lemma filter_lt_of_ge {n m l : ℕ} (hlm : l ≤ m) : (Ico n m).filter (λ x, x < l) = Ico n l := -congr_arg coe $ list.Ico.filter_lt_of_ge hlm - -@[simp] lemma filter_lt (n m l : ℕ) : (Ico n m).filter (λ x, x < l) = Ico n (min m l) := -congr_arg coe $ list.Ico.filter_lt n m l - -lemma filter_le_of_le_bot {n m l : ℕ} (hln : l ≤ n) : (Ico n m).filter (λ x, l ≤ x) = Ico n m := -congr_arg coe $ list.Ico.filter_le_of_le_bot hln - -lemma filter_le_of_top_le {n m l : ℕ} (hml : m ≤ l) : (Ico n m).filter (λ x, l ≤ x) = ∅ := -congr_arg coe $ list.Ico.filter_le_of_top_le hml - -lemma filter_le_of_le {n m l : ℕ} (hnl : n ≤ l) : (Ico n m).filter (λ x, l ≤ x) = Ico l m := -congr_arg coe $ list.Ico.filter_le_of_le hnl - -@[simp] lemma filter_le (n m l : ℕ) : (Ico n m).filter (λ x, l ≤ x) = Ico (max n l) m := -congr_arg coe $ list.Ico.filter_le n m l - -end Ico -end multiset diff --git a/src/data/multiset/locally_finite.lean b/src/data/multiset/locally_finite.lean index 5df9bcd6159fd..bbb96e7279f3d 100644 --- a/src/data/multiset/locally_finite.lean +++ b/src/data/multiset/locally_finite.lean @@ -10,25 +10,25 @@ 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] @@ -36,20 +36,59 @@ by rw [Ioc, finset.val_eq_zero, finset.Ioc_eq_empty_iff] 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 @@ -57,8 +96,56 @@ 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 α] @@ -66,6 +153,10 @@ 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 _ _ _ } diff --git a/src/data/nat/interval.lean b/src/data/nat/interval.lean index de4b5430aafc0..8f08f8d3eee89 100644 --- a/src/data/nat/interval.lean +++ b/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,14 +103,11 @@ 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] } @@ -120,8 +115,7 @@ 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] }, diff --git a/src/order/locally_finite.lean b/src/order/locally_finite.lean index b6dfce353f8d9..2826a2aeee00e 100644 --- a/src/order/locally_finite.lean +++ b/src/order/locally_finite.lean @@ -28,7 +28,7 @@ In a `locally_finite_order`, * `finset.Ioc`: Open-closed interval as a finset. * `finset.Ioo`: Open-open interval as a finset. * `multiset.Icc`: Closed-closed interval as a multiset. -* `multiset.Ico`: Closed-open interval as a multiset. Currently only for `ℕ`. +* `multiset.Ico`: Closed-open interval as a multiset. * `multiset.Ioc`: Open-closed interval as a multiset. * `multiset.Ioo`: Open-open interval as a multiset. @@ -64,8 +64,6 @@ Along, you will find lemmas about the cardinality of those finite intervals. ## TODO -`multiset.Ico` hasn't been generalized yet. All of `data.multiset.intervals` should be generalized. - Provide the `locally_finite_order` instance for `lex α β` where `locally_finite_order α` and `fintype β`. @@ -76,8 +74,7 @@ From `linear_order α`, `no_top_order α`, `locally_finite_order α`, we can als order isomorphism `α ≃ ℕ` or `α ≃ ℤ`, depending on whether we have `order_bot α` or `no_bot_order α` and `nonempty α`. When `order_bot α`, we can match `a : α` to `(Iio a).card`. -Once we have the `succ_order` typeclass (any non-top element has a least greater element), we -can provide `succ_order α` from `linear_order α` and `locally_finite_order α` using +We can provide `succ_order α` from `linear_order α` and `locally_finite_order α` using ```lean lemma exists_min_greater [linear_order α] [locally_finite_order α] {x ub : α} (hx : x < ub) : @@ -261,7 +258,9 @@ variables [preorder α] [locally_finite_order α] multiset. -/ def Icc (a b : α) : multiset α := (finset.Icc a b).val --- TODO@Yaël: Nuke `data.multiset.intervals` and redefine `multiset.Ico` here +/-- The multiset of elements `x` such that `a ≤ x` and `x < b`. Basically `set.Ico a b` as a +multiset. -/ +def Ico (a b : α) : multiset α := (finset.Ico a b).val /-- The multiset of elements `x` such that `a < x` and `x ≤ b`. Basically `set.Ioc a b` as a multiset. -/ @@ -274,6 +273,9 @@ def Ioo (a b : α) : multiset α := (finset.Ioo a b).val @[simp] lemma mem_Icc {a b x : α} : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b := by rw [Icc, ←finset.mem_def, finset.mem_Icc] +@[simp] lemma mem_Ico {a b x : α} : x ∈ Ico a b ↔ a ≤ x ∧ x < b := +by rw [Ico, ←finset.mem_def, finset.mem_Ico] + @[simp] lemma mem_Ioc {a b x : α} : x ∈ Ioc a b ↔ a < x ∧ x ≤ b := by rw [Ioc, ←finset.mem_def, finset.mem_Ioc] @@ -306,7 +308,6 @@ def Iic (b : α) : multiset α := (finset.Iic b).val def Iio (b : α) : multiset α := (finset.Iio b).val @[simp] lemma mem_Iic {b x : α} : x ∈ Iic b ↔ x ≤ b := by rw [Iic, ←finset.mem_def, finset.mem_Iic] - @[simp] lemma mem_Iio {b x : α} : x ∈ Iio b ↔ x < b := by rw [Iio, ←finset.mem_def, finset.mem_Iio] end order_bot @@ -330,17 +331,10 @@ fintype.of_finset (finset.Ioc a b) (λ x, by rw [finset.mem_Ioc, mem_Ioc]) instance fintype_Ioo : fintype (Ioo a b) := fintype.of_finset (finset.Ioo a b) (λ x, by rw [finset.mem_Ioo, mem_Ioo]) -lemma finite_Icc : (Icc a b).finite := -⟨set.fintype_Icc a b⟩ - -lemma finite_Ico : (Ico a b).finite := -⟨set.fintype_Ico a b⟩ - -lemma finite_Ioc : (Ioc a b).finite := -⟨set.fintype_Ioc a b⟩ - -lemma finite_Ioo : (Ioo a b).finite := -⟨set.fintype_Ioo a b⟩ +lemma finite_Icc : (Icc a b).finite := ⟨set.fintype_Icc a b⟩ +lemma finite_Ico : (Ico a b).finite := ⟨set.fintype_Ico a b⟩ +lemma finite_Ioc : (Ioc a b).finite := ⟨set.fintype_Ioc a b⟩ +lemma finite_Ioo : (Ioo a b).finite := ⟨set.fintype_Ioo a b⟩ end preorder @@ -354,7 +348,6 @@ instance fintype_Ioi : fintype (Ioi a) := fintype.of_finset (finset.Ioi a) (λ x, by rw [finset.mem_Ioi, mem_Ioi]) lemma finite_Ici : (Ici a).finite := ⟨set.fintype_Ici a⟩ - lemma finite_Ioi : (Ioi a).finite := ⟨set.fintype_Ioi a⟩ end order_top @@ -369,7 +362,6 @@ instance fintype_Iio : fintype (Iio b) := fintype.of_finset (finset.Iio b) (λ x, by rw [finset.mem_Iio, mem_Iio]) lemma finite_Iic : (Iic b).finite := ⟨set.fintype_Iic b⟩ - lemma finite_Iio : (Iio b).finite := ⟨set.fintype_Iio b⟩ end order_bot @@ -391,8 +383,7 @@ noncomputable def locally_finite_order.of_finite_Icc (h : ∀ a b : α, (set.Icc (λ a b x, by rw [set.finite.mem_to_finset, set.mem_Icc]) /-- A fintype is noncomputably a locally finite order. -/ -noncomputable def fintype.to_locally_finite_order [fintype α] : - locally_finite_order α := +noncomputable def fintype.to_locally_finite_order [fintype α] : locally_finite_order α := { finset_Icc := λ a b, (set.finite.of_fintype (set.Icc a b)).to_finset, finset_Ico := λ a b, (set.finite.of_fintype (set.Ico a b)).to_finset, finset_Ioc := λ a b, (set.finite.of_fintype (set.Ioc a b)).to_finset, @@ -421,8 +412,7 @@ variables [preorder β] [locally_finite_order β] -- Should this be called `locally_finite_order.lift`? /-- Given an order embedding `α ↪o β`, pulls back the `locally_finite_order` on `β` to `α`. -/ -noncomputable def order_embedding.locally_finite_order (f : α ↪o β) : - locally_finite_order α := +noncomputable def order_embedding.locally_finite_order (f : α ↪o β) : locally_finite_order α := { finset_Icc := λ a b, (Icc (f a) (f b)).preimage f (f.to_embedding.injective.inj_on _), finset_Ico := λ a b, (Ico (f a) (f b)).preimage f (f.to_embedding.injective.inj_on _), finset_Ioc := λ a b, (Ioc (f a) (f b)).preimage f (f.to_embedding.injective.inj_on _),