From 957fa4bb292a70161679811a0bd2309aee5a8351 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 29 Nov 2021 09:57:02 +0000 Subject: [PATCH] =?UTF-8?q?feat(order/locally=5Ffinite):=20`with=5Ftop=20?= =?UTF-8?q?=CE=B1`/`with=5Fbot=20=CE=B1`=20are=20locally=20finite=20orders?= =?UTF-8?q?=20(#10202)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This provides the two instances `locally_finite_order (with_top α)` and `locally_finite_order (with_bot α)`. Co-authored-by: Adam Topaz --- src/data/finset/basic.lean | 2 + src/data/option/defs.lean | 2 + src/logic/embedding.lean | 10 +++- src/order/locally_finite.lean | 109 +++++++++++++++++++++++++++++++++- 4 files changed, 121 insertions(+), 2 deletions(-) diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index 519c0618090f7..675a79eb596dd 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -483,6 +483,8 @@ def cons {α} (a : α) (s : finset α) (h : a ∉ s) : finset α := @[simp] theorem mem_cons {a s h b} : b ∈ @cons α a s h ↔ b = a ∨ b ∈ s := by rcases s with ⟨⟨s⟩⟩; apply list.mem_cons_iff +@[simp] lemma mem_cons_self (a : α) (s : finset α) {h} : a ∈ cons a s h := mem_cons.2 $ or.inl rfl + @[simp] theorem cons_val {a : α} {s : finset α} (h : a ∉ s) : (cons a s h).1 = a ::ₘ s.1 := rfl @[simp] theorem mk_cons {a : α} {s : multiset α} (h : (a ::ₘ s).nodup) : diff --git a/src/data/option/defs.lean b/src/data/option/defs.lean index a358017e698f8..93e79f0e0d182 100644 --- a/src/data/option/defs.lean +++ b/src/data/option/defs.lean @@ -28,6 +28,8 @@ instance has_mem : has_mem α (option α) := ⟨λ a b, b = some a⟩ @[simp] theorem mem_def {a : α} {b : option α} : a ∈ b ↔ b = some a := iff.rfl +lemma mem_iff {a : α} {b : option α} : a ∈ b ↔ b = a := iff.rfl + theorem is_none_iff_eq_none {o : option α} : o.is_none = tt ↔ o = none := ⟨option.eq_none_of_is_none, λ e, e.symm ▸ rfl⟩ diff --git a/src/logic/embedding.lean b/src/logic/embedding.lean index 45598d001b091..f43d3e88b7f57 100644 --- a/src/logic/embedding.lean +++ b/src/logic/embedding.lean @@ -148,10 +148,18 @@ theorem set_value_eq {α β} (f : α ↪ β) (a : α) (b : β) [∀ a', decidabl [∀ a', decidable (f a' = b)] : set_value f a b a = b := by simp [set_value] -/-- Embedding into `option` -/ +/-- Embedding into `option α` using `some`. -/ @[simps { fully_applied := ff }] protected def some {α} : α ↪ option α := ⟨some, option.some_injective α⟩ +/-- Embedding into `option α` using `coe`. Usually the correct synctatical form for `simp`. -/ +@[simps { fully_applied := ff }] +def coe_option {α} : α ↪ option α := ⟨coe, option.some_injective α⟩ + +/-- Embedding into `with_top α`. -/ +@[simps] +def coe_with_top {α} : α ↪ with_top α := { to_fun := coe, ..embedding.some} + /-- Given an embedding `f : α ↪ β` and a point outside of `set.range f`, construct an embedding `option α ↪ β`. -/ @[simps] def option_elim {α β} (f : α ↪ β) (x : β) (h : x ∉ set.range f) : diff --git a/src/order/locally_finite.lean b/src/order/locally_finite.lean index 0362ce9a3b069..cacbf142281fb 100644 --- a/src/order/locally_finite.lean +++ b/src/order/locally_finite.lean @@ -97,7 +97,7 @@ successor (and actually a predecessor as well), so it is a `succ_order`, but it' as `Icc (-1) 1` is infinite. -/ -open finset +open finset function /-- A locally finite order is an order where bounded intervals are finite. When you don't care too much about definitional equality, you can use `locally_finite_order.of_Icc` or @@ -482,6 +482,113 @@ locally_finite_order.of_Icc' (α × β) end preorder +/-! +#### `with_top`, `with_bot` + +Adding a `⊤` to a locally finite `order_top` keeps it locally finite. +Adding a `⊥` to a locally finite `order_bot` keeps it locally finite. +-/ + +namespace with_top +variables (α) [partial_order α] [order_top α] [locally_finite_order α] + +local attribute [pattern] coe +local attribute [simp] option.mem_iff + +instance : locally_finite_order (with_top α) := +{ finset_Icc := λ a b, match a, b with + | ⊤, ⊤ := {⊤} + | ⊤, (b : α) := ∅ + | (a : α), ⊤ := insert_none (Ici a) + | (a : α), (b : α) := (Icc a b).map embedding.coe_option + end, + finset_Ico := λ a b, match a, b with + | ⊤, _ := ∅ + | (a : α), ⊤ := (Ici a).map embedding.coe_option + | (a : α), (b : α) := (Ico a b).map embedding.coe_option + end, + finset_Ioc := λ a b, match a, b with + | ⊤, _ := ∅ + | (a : α), ⊤ := insert_none (Ioi a) + | (a : α), (b : α) := (Ioc a b).map embedding.coe_option + end, + finset_Ioo := λ a b, match a, b with + | ⊤, _ := ∅ + | (a : α), ⊤ := (Ioi a).map embedding.coe_option + | (a : α), (b : α) := (Ioo a b).map embedding.coe_option + end, + finset_mem_Icc := λ a b x, match a, b, x with + | ⊤, ⊤, x := mem_singleton.trans (le_antisymm_iff.trans $ and_comm _ _) + | ⊤, (b : α), x := iff_of_false (not_mem_empty _) + (λ h, (h.1.trans h.2).not_lt $ coe_lt_top _) + | (a : α), ⊤, ⊤ := by simp [with_top.locally_finite_order._match_1] + | (a : α), ⊤, (x : α) := by simp [with_top.locally_finite_order._match_1, coe_eq_coe] + | (a : α), (b : α), ⊤ := by simp [with_top.locally_finite_order._match_1] + | (a : α), (b : α), (x : α) := by simp [with_top.locally_finite_order._match_1, coe_eq_coe] + end, + finset_mem_Ico := λ a b x, match a, b, x with + | ⊤, b, x := iff_of_false (not_mem_empty _) + (λ h, not_top_lt $ h.1.trans_lt h.2) + | (a : α), ⊤, ⊤ := by simp [with_top.locally_finite_order._match_2] + | (a : α), ⊤, (x : α) := by simp [with_top.locally_finite_order._match_2, coe_eq_coe, + coe_lt_top] + | (a : α), (b : α), ⊤ := by simp [with_top.locally_finite_order._match_2] + | (a : α), (b : α), (x : α) := by simp [with_top.locally_finite_order._match_2, coe_eq_coe, + coe_lt_coe] + end, + finset_mem_Ioc := λ a b x, match a, b, x with + | ⊤, b, x := iff_of_false (not_mem_empty _) + (λ h, not_top_lt $ h.1.trans_le h.2) + | (a : α), ⊤, ⊤ := by simp [with_top.locally_finite_order._match_3, coe_lt_top] + | (a : α), ⊤, (x : α) := by simp [with_top.locally_finite_order._match_3, coe_eq_coe, + coe_lt_coe] + | (a : α), (b : α), ⊤ := by simp [with_top.locally_finite_order._match_3] + | (a : α), (b : α), (x : α) := by simp [with_top.locally_finite_order._match_3, coe_eq_coe, + coe_lt_coe] + end, + finset_mem_Ioo := λ a b x, match a, b, x with + | ⊤, b, x := iff_of_false (not_mem_empty _) + (λ h, not_top_lt $ h.1.trans h.2) + | (a : α), ⊤, ⊤ := by simp [with_top.locally_finite_order._match_4, coe_lt_top] + | (a : α), ⊤, (x : α) := by simp [with_top.locally_finite_order._match_4, coe_eq_coe, + coe_lt_coe, coe_lt_top] + | (a : α), (b : α), ⊤ := by simp [with_top.locally_finite_order._match_4] + | (a : α), (b : α), (x : α) := by simp [with_top.locally_finite_order._match_4, coe_eq_coe, + coe_lt_coe] + end } + +variables (a b : α) + +lemma Icc_coe_top : Icc (a : with_top α) ⊤ = insert_none (Ici a) := rfl +lemma Icc_coe_coe : Icc (a : with_top α) b = (Icc a b).map embedding.coe_option := rfl +lemma Ico_coe_top : Ico (a : with_top α) ⊤ = (Ici a).map embedding.coe_option := rfl +lemma Ico_coe_coe : Ico (a : with_top α) b = (Ico a b).map embedding.coe_option := rfl +lemma Ioc_coe_top : Ioc (a : with_top α) ⊤ = insert_none (Ioi a) := rfl +lemma Ioc_coe_coe : Ioc (a : with_top α) b = (Ioc a b).map embedding.coe_option := rfl +lemma Ioo_coe_top : Ioo (a : with_top α) ⊤ = (Ioi a).map embedding.coe_option := rfl +lemma Ioo_coe_coe : Ioo (a : with_top α) b = (Ioo a b).map embedding.coe_option := rfl + +end with_top + +namespace with_bot +variables (α) [partial_order α] [order_bot α] [locally_finite_order α] + +instance : locally_finite_order (with_bot α) := +@order_dual.locally_finite_order (with_top (order_dual α)) _ _ + +variables (a b : α) + +lemma Icc_bot_coe : Icc (⊥ : with_bot α) b = insert_none (Iic b) := rfl +lemma Icc_coe_coe : Icc (a : with_bot α) b = (Icc a b).map embedding.coe_option := rfl +lemma Ico_bot_coe : Ico (⊥ : with_bot α) b = insert_none (Iio b) := rfl +lemma Ico_coe_coe : Ico (a : with_bot α) b = (Ico a b).map embedding.coe_option := rfl +lemma Ioc_bot_coe : Ioc (⊥ : with_bot α) b = (Iic b).map embedding.coe_option := rfl +lemma Ioc_coe_coe : Ioc (a : with_bot α) b = (Ioc a b).map embedding.coe_option := rfl +lemma Ioo_bot_coe : Ioo (⊥ : with_bot α) b = (Iio b).map embedding.coe_option := rfl +lemma Ioo_coe_coe : Ioo (a : with_bot α) b = (Ioo a b).map embedding.coe_option := rfl + +end with_bot + /-! #### Subtype of a locally finite order -/ variables [preorder α] [locally_finite_order α] (p : α → Prop) [decidable_pred p]