feat(order/conditionally_complete_lattice): conditional Inf of interv…

…als (#7226)

Some new simp lemmas for cInf/cSup of intervals. I tried to use the minimal possible assumptions that I could - some lemmas are therefore in the linear order section and others are just for lattices.

src/order/bounds.lean

@@ -413,27 +413,35 @@ lemma lower_bounds_Ico (h : a < b) : lower_bounds (Ico a b) = Iic a :=
 
 section
 
-variables [linear_order γ] [densely_ordered γ]
+variables [semilattice_sup γ] [densely_ordered γ]
 
-lemma is_glb_Ioo {a b : γ} (hab : a < b) : is_glb (Ioo a b) a :=
+lemma is_glb_Ioo {a b : γ} (h : a < b) :
+  is_glb (Ioo a b) a :=
+⟨λ x hx, hx.1.le, λ x hx,
 begin
-  refine ⟨λx hx, le_of_lt hx.1, λy hy, le_of_not_lt $ λ h, _⟩,
-  have : a < min b y, by { rw lt_min_iff, exact ⟨hab, h⟩ },
-  rcases exists_between this with ⟨z, az, zy⟩,
-  rw lt_min_iff at zy,
-  exact lt_irrefl _ (lt_of_le_of_lt (hy ⟨az, zy.1⟩) zy.2)
-end
+  cases eq_or_lt_of_le (le_sup_right : a ≤ x ⊔ a) with h₁ h₂,
+  { exact h₁.symm ▸ le_sup_left },
+  obtain ⟨y, lty, ylt⟩ := exists_between h₂,
+  apply (not_lt_of_le (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim,
+  obtain ⟨u, au, ub⟩ := exists_between h,
+  apply (hx ⟨au, ub⟩).trans ub.le,
+end⟩
 
 lemma lower_bounds_Ioo {a b : γ} (hab : a < b) : lower_bounds (Ioo a b) = Iic a :=
 (is_glb_Ioo hab).lower_bounds_eq
 
 lemma is_glb_Ioc {a b : γ} (hab : a < b) : is_glb (Ioc a b) a :=
-(is_glb_Ioo hab).of_subset_of_superset (is_glb_Icc $ le_of_lt hab)
-  Ioo_subset_Ioc_self Ioc_subset_Icc_self
+(is_glb_Ioo hab).of_subset_of_superset (is_glb_Icc hab.le) Ioo_subset_Ioc_self Ioc_subset_Icc_self
 
 lemma lower_bound_Ioc {a b : γ} (hab : a < b) : lower_bounds (Ioc a b) = Iic a :=
 (is_glb_Ioc hab).lower_bounds_eq
 
+end
+
+section
+
+variables [semilattice_inf γ] [densely_ordered γ]
+
 lemma is_lub_Ioo {a b : γ} (hab : a < b) : is_lub (Ioo a b) b :=
 by simpa only [dual_Ioo] using @is_glb_Ioo (order_dual γ) _ _ b a hab
 

src/order/conditionally_complete_lattice.lean

@@ -278,10 +278,40 @@ nonempty and bounded below.-/
 theorem cInf_insert (hs : bdd_below s) (sne : s.nonempty) : Inf (insert a s) = a ⊓ Inf s :=
 ((is_glb_cInf sne hs).insert a).cInf_eq (insert_nonempty a s)
 
+@[simp] lemma cInf_Icc (h : a ≤ b) : Inf (Icc a b) = a :=
+(is_glb_Icc h).cInf_eq (nonempty_Icc.2 h)
+
 @[simp] lemma cInf_Ici : Inf (Ici a) = a := is_least_Ici.cInf_eq
 
+@[simp] lemma cInf_Ico (h : a < b) : Inf (Ico a b) = a :=
+(is_glb_Ico h).cInf_eq (nonempty_Ico.2 h)
+
+@[simp] lemma cInf_Ioc [densely_ordered α] (h : a < b) : Inf (Ioc a b) = a :=
+(is_glb_Ioc h).cInf_eq (nonempty_Ioc.2 h)
+
+@[simp] lemma cInf_Ioi [no_top_order α] [densely_ordered α] : Inf (Ioi a) = a :=
+cInf_intro nonempty_Ioi (λ _, le_of_lt) (λ w hw, by simpa using exists_between hw)
+
+@[simp] lemma cInf_Ioo [densely_ordered α] (h : a < b) : Inf (Ioo a b) = a :=
+(is_glb_Ioo h).cInf_eq (nonempty_Ioo.2 h)
+
+@[simp] lemma cSup_Icc (h : a ≤ b) : Sup (Icc a b) = b :=
+(is_lub_Icc h).cSup_eq (nonempty_Icc.2 h)
+
+@[simp] lemma cSup_Ico [densely_ordered α] (h : a < b) : Sup (Ico a b) = b :=
+(is_lub_Ico h).cSup_eq (nonempty_Ico.2 h)
+
 @[simp] lemma cSup_Iic : Sup (Iic a) = a := is_greatest_Iic.cSup_eq
 
+@[simp] lemma cSup_Iio [no_bot_order α] [densely_ordered α] : Sup (Iio a) = a :=
+cSup_intro nonempty_Iio (λ _, le_of_lt) (λ w hw, by simpa [and_comm] using exists_between hw)
+
+@[simp] lemma cSup_Ioc (h : a < b) : Sup (Ioc a b) = b :=
+(is_lub_Ioc h).cSup_eq (nonempty_Ioc.2 h)
+
+@[simp] lemma cSup_Ioo [densely_ordered α] (h : a < b) : Sup (Ioo a b) = b :=
+(is_lub_Ioo h).cSup_eq (nonempty_Ioo.2 h)
+
 /--The indexed supremum of two functions are comparable if the functions are pointwise comparable-/
 lemma csupr_le_csupr {f g : ι → α} (B : bdd_above (range g)) (H : ∀x, f x ≤ g x) :
   supr f ≤ supr g :=