From 18dce13469f01e0126abb2966ecfc310e7ff3bcc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 28 Oct 2021 18:57:46 +0000
Subject: [PATCH] feat(data/finset/interval): Bounded intervals in locally
 finite orders are finite (#9960)

A set which is bounded above and below is finite. A set which is bounded below in an `order_top` is finite. A set which is bounded above in an `order_bot` is finite.

Also provide the `order_dual` constructions for `bdd_stuff` and `locally_finite_order`.
---
 src/data/finset/locally_finite.lean | 24 +++++++++++++
 src/order/bounds.lean               | 30 ++++++++++------
 src/order/locally_finite.lean       | 53 ++++++++++++++++++++++++++++-
 3 files changed, 95 insertions(+), 12 deletions(-)

diff --git a/src/data/finset/locally_finite.lean b/src/data/finset/locally_finite.lean
index 94fabc456a29d..015ea0b57e38e 100644
--- a/src/data/finset/locally_finite.lean
+++ b/src/data/finset/locally_finite.lean
@@ -112,6 +112,15 @@ begin
   exact and_iff_right_of_imp (λ h, hac.trans h.1),
 end
 
+/-- A set with upper and lower bounds in a locally finite order is a fintype -/
+def _root_.set.fintype_of_mem_bounds {a b} {s : set α} [decidable_pred (∈ s)]
+  (ha : a ∈ lower_bounds s) (hb : b ∈ upper_bounds s) : fintype s :=
+set.fintype_subset (set.Icc a b) $ λ x hx, ⟨ha hx, hb hx⟩
+
+lemma _root_.bdd_below.finite_of_bdd_above {s : set α} (h₀ : bdd_below s) (h₁ : bdd_above s) :
+  s.finite :=
+let ⟨a, ha⟩ := h₀, ⟨b, hb⟩ := h₁ in by { classical, exact ⟨set.fintype_of_mem_bounds ha hb⟩ }
+
 end preorder
 
 section partial_order
@@ -202,6 +211,21 @@ end
 
 end linear_order
 
+section order_top
+variables [order_top α] [locally_finite_order α]
+
+lemma _root_.bdd_below.finite {s : set α} (hs : bdd_below s) : s.finite :=
+hs.finite_of_bdd_above $ order_top.bdd_above s
+
+end order_top
+
+section order_bot
+variables [order_bot α] [locally_finite_order α]
+
+lemma _root_.bdd_above.finite {s : set α} (hs : bdd_above s) : s.finite := hs.dual.finite
+
+end order_bot
+
 section ordered_cancel_add_comm_monoid
 variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] [decidable_eq α]
   [locally_finite_order α]
diff --git a/src/order/bounds.lean b/src/order/bounds.lean
index b21866f407970..a44eb57c274d3 100644
--- a/src/order/bounds.lean
+++ b/src/order/bounds.lean
@@ -82,6 +82,18 @@ lemma not_bdd_below_iff {α : Type*} [linear_order α] {s : set α} :
   ¬bdd_below s ↔ ∀ x, ∃ y ∈ s, y < x :=
 @not_bdd_above_iff (order_dual α) _ _
 
+lemma bdd_above.dual (h : bdd_above s) : bdd_below (of_dual ⁻¹' s) := h
+
+lemma bdd_below.dual (h : bdd_below s) : bdd_above (of_dual ⁻¹' s) := h
+
+lemma is_least.dual (h : is_least s a) : is_greatest (of_dual ⁻¹' s) (to_dual a) := h
+
+lemma is_greatest.dual (h : is_greatest s a) : is_least (of_dual ⁻¹' s) (to_dual a) := h
+
+lemma is_lub.dual (h : is_lub s a) : is_glb (of_dual ⁻¹' s) (to_dual a) := h
+
+lemma is_glb.dual (h : is_glb s a) : is_lub (of_dual ⁻¹' s) (to_dual a) := h
+
 /-!
 ### Monotonicity
 -/
@@ -126,7 +138,7 @@ lemma is_lub.of_subset_of_superset {s t p : set α} (hs : is_lub s a) (hp : is_l
 set `t`, `s ⊆ t ⊆ p`. -/
 lemma is_glb.of_subset_of_superset {s t p : set α} (hs : is_glb s a) (hp : is_glb p a)
   (hst : s ⊆ t) (htp : t ⊆ p) : is_glb t a :=
-@is_lub.of_subset_of_superset (order_dual α) _ a s t p hs hp hst htp
+hs.dual.of_subset_of_superset hp hst htp
 
 lemma is_least.mono (ha : is_least s a) (hb : is_least t b) (hst : s ⊆ t) : b ≤ a :=
 hb.2 (hst ha.1)
@@ -163,8 +175,7 @@ lemma is_greatest.is_lub (h : is_greatest s a) : is_lub s a := ⟨h.2, λ b hb,
 lemma is_lub.upper_bounds_eq (h : is_lub s a) : upper_bounds s = Ici a :=
 set.ext $ λ b, ⟨λ hb, h.2 hb, λ hb, upper_bounds_mono_mem hb h.1⟩
 
-lemma is_glb.lower_bounds_eq (h : is_glb s a) : lower_bounds s = Iic a :=
-@is_lub.upper_bounds_eq (order_dual α) _ _ _ h
+lemma is_glb.lower_bounds_eq (h : is_glb s a) : lower_bounds s = Iic a := h.dual.upper_bounds_eq
 
 lemma is_least.lower_bounds_eq (h : is_least s a) : lower_bounds s = Iic a :=
 h.is_glb.lower_bounds_eq
@@ -287,7 +298,7 @@ then `a ⊓ b` is the greatest lower bound of `s ∪ t`. -/
 lemma is_glb.union [semilattice_inf γ] {a₁ a₂ : γ} {s t : set γ}
   (hs : is_glb s a₁) (ht : is_glb t a₂) :
   is_glb (s ∪ t) (a₁ ⊓ a₂) :=
-@is_lub.union (order_dual γ) _ _ _ _ _ hs ht
+hs.dual.union ht
 
 /-- If `a` is the least element of `s` and `b` is the least element of `t`,
 then `min a b` is the least element of `s ∪ t`. -/
@@ -310,7 +321,7 @@ lemma is_lub.inter_Ici_of_mem [linear_order γ] {s : set γ} {a b : γ} (ha : is
 
 lemma is_glb.inter_Iic_of_mem [linear_order γ] {s : set γ} {a b : γ} (ha : is_glb s a)
   (hb : b ∈ s) : is_glb (s ∩ Iic b) a :=
-@is_lub.inter_Ici_of_mem (order_dual γ) _ _ _ _ ha hb
+ha.dual.inter_Ici_of_mem hb
 
 /-!
 ### Specific sets
@@ -545,8 +556,7 @@ ne_empty_iff_nonempty.1 $ assume h,
 have a ≤ a', from hs.right $ by simp only [h, upper_bounds_empty],
 not_le_of_lt ha' this
 
-lemma is_glb.nonempty [no_top_order α] (hs : is_glb s a) : s.nonempty :=
-@is_lub.nonempty (order_dual α) _ _ _ _ hs
+lemma is_glb.nonempty [no_top_order α] (hs : is_glb s a) : s.nonempty := hs.dual.nonempty
 
 lemma nonempty_of_not_bdd_above [ha : nonempty α] (h : ¬bdd_above s) : s.nonempty :=
 nonempty.elim ha $ λ x, (not_bdd_above_iff'.1 h x).imp $ λ a ha, ha.fst
@@ -653,8 +663,7 @@ lower_bounds_le_upper_bounds ha.1 hb.1 hs
 lemma is_lub_lt_iff (ha : is_lub s a) : a < b ↔ ∃ c ∈ upper_bounds s, c < b :=
 ⟨λ hb, ⟨a, ha.1, hb⟩, λ ⟨c, hcs, hcb⟩, lt_of_le_of_lt (ha.2 hcs) hcb⟩
 
-lemma lt_is_glb_iff (ha : is_glb s a) : b < a ↔ ∃ c ∈ lower_bounds s, b < c :=
-@is_lub_lt_iff (order_dual α) _ s _ _ ha
+lemma lt_is_glb_iff (ha : is_glb s a) : b < a ↔ ∃ c ∈ lower_bounds s, b < c := is_lub_lt_iff ha.dual
 
 lemma le_of_is_lub_le_is_glb {x y} (ha : is_glb s a) (hb : is_lub s b) (hab : b ≤ a)
   (hx : x ∈ s) (hy : y ∈ s) : x ≤ y :=
@@ -705,8 +714,7 @@ variables [linear_order α] {s : set α} {a b : α}
 lemma lt_is_lub_iff (h : is_lub s a) : b < a ↔ ∃ c ∈ s, b < c :=
 by simp only [← not_le, is_lub_le_iff h, mem_upper_bounds, not_forall]
 
-lemma is_glb_lt_iff (h : is_glb s a) : a < b ↔ ∃ c ∈ s, c < b :=
-@lt_is_lub_iff (order_dual α) _ _ _ _ h
+lemma is_glb_lt_iff (h : is_glb s a) : a < b ↔ ∃ c ∈ s, c < b := lt_is_lub_iff h.dual
 
 lemma is_lub.exists_between (h : is_lub s a) (hb : b < a) :
   ∃ c ∈ s, b < c ∧ c ≤ a :=
diff --git a/src/order/locally_finite.lean b/src/order/locally_finite.lean
index 6738006a8eb73..45923a19caf0a 100644
--- a/src/order/locally_finite.lean
+++ b/src/order/locally_finite.lean
@@ -462,7 +462,58 @@ noncomputable def order_embedding.locally_finite_order (f : α ↪o β) :
   finset_mem_Ioc := λ a b x, by rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le],
   finset_mem_Ioo := λ a b x, by rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt] }
 
-variables [locally_finite_order α]
+open order_dual
+
+variables [locally_finite_order α] (a b : α)
+
+/-- Note we define `Icc (to_dual a) (to_dual b)` as `Icc α _ _ b a` (which has type `finset α` not
+`finset (order_dual α)`!) instead of `(Icc b a).map to_dual.to_embedding` as this means the
+following is defeq:
+```
+lemma this : (Icc (to_dual (to_dual a)) (to_dual (to_dual b)) : _) = (Icc a b : _) := rfl
+```
+-/
+instance : locally_finite_order (order_dual α) :=
+{ finset_Icc := λ a b, @Icc α _ _ (of_dual b) (of_dual a),
+  finset_Ico := λ a b, @Ioc α _ _ (of_dual b) (of_dual a),
+  finset_Ioc := λ a b, @Ico α _ _ (of_dual b) (of_dual a),
+  finset_Ioo := λ a b, @Ioo α _ _ (of_dual b) (of_dual a),
+  finset_mem_Icc := λ a b x, mem_Icc.trans (and_comm _ _),
+  finset_mem_Ico := λ a b x, mem_Ioc.trans (and_comm _ _),
+  finset_mem_Ioc := λ a b x, mem_Ico.trans (and_comm _ _),
+  finset_mem_Ioo := λ a b x, mem_Ioo.trans (and_comm _ _) }
+
+lemma Icc_to_dual : Icc (to_dual a) (to_dual b) = (Icc b a).map to_dual.to_embedding :=
+begin
+  refine eq.trans _ map_refl.symm,
+  ext c,
+  rw [mem_Icc, mem_Icc],
+  exact and_comm _ _,
+end
+
+lemma Ico_to_dual : Ico (to_dual a) (to_dual b) = (Ioc b a).map to_dual.to_embedding :=
+begin
+  refine eq.trans _ map_refl.symm,
+  ext c,
+  rw [mem_Ico, mem_Ioc],
+  exact and_comm _ _,
+end
+
+lemma Ioc_to_dual : Ioc (to_dual a) (to_dual b) = (Ico b a).map to_dual.to_embedding :=
+begin
+  refine eq.trans _ map_refl.symm,
+  ext c,
+  rw [mem_Ioc, mem_Ico],
+  exact and_comm _ _,
+end
+
+lemma Ioo_to_dual : Ioo (to_dual a) (to_dual b) = (Ioo b a).map to_dual.to_embedding :=
+begin
+  refine eq.trans _ map_refl.symm,
+  ext c,
+  rw [mem_Ioo, mem_Ioo],
+  exact and_comm _ _,
+end
 
 instance [decidable_rel ((≤) : α × β → α × β → Prop)] : locally_finite_order (α × β) :=
 locally_finite_order.of_Icc' (α × β)