feat(order/locally_finite): with_top α/with_bot α are locally fin…

…ite orders (#10202)

This provides the two instances `locally_finite_order (with_top α)` and `locally_finite_order (with_bot α)`.



Co-authored-by: Adam Topaz <github@adamtopaz.com>

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) :

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⟩
 

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) :

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]