feat(Order/CompleteLatticeIntervals): ConditionallyCompleteLinearOrderBot for Set.Iio

Mathlib/Order/Bounds/Basic.lean

@@ -324,6 +324,10 @@ theorem BddAbove.exists_ge [SemilatticeSup γ] {s : Set γ} (hs : BddAbove s) (x
 theorem isLeast_Ici : IsLeast (Ici a) a :=
   ⟨self_mem_Ici, fun _ => id⟩
 
+@[to_dual]
+theorem isGreatest_Ioi_top [OrderTop α] (ha : ¬ IsMax a) : IsGreatest (Ioi a) ⊤ :=
+  ⟨(not_isMax_iff.1 ha).elim fun _ => lt_top_of_lt, fun _ _ => le_top⟩
+
 @[to_dual]
 theorem isLUB_Iic : IsLUB (Iic a) a :=
   isGreatest_Iic.isLUB

Mathlib/Order/CompleteLatticeIntervals.lean

@@ -166,6 +166,58 @@ noncomputable instance ordConnectedSubsetConditionallyCompleteLinearOrder [Inhab
 
 end OrdConnected
 
+section Iio
+
+open Classical in
+/-- Complete linear order structure on `Set.Iio` -/
+noncomputable instance Set.Iio.conditionallyCompleteLinearOrderBot
+    [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)] :
+    ConditionallyCompleteLinearOrderBot (Iio a) where
+  __ := (inferInstance : LinearOrder (Iio a))
+  __ := orderBot
+  __ := (inferInstance : Lattice (Iio a))
+  sSup S := if hS : BddAbove S then ⟨sSup ((↑) '' S), by
+    rcases hS with ⟨b, hb⟩
+    rw [mem_Iio]
+    apply b.2.trans_le'
+    apply csSup_le'
+    simpa [mem_upperBounds] using hb⟩ else ⊥
+  isLUB_csSup S hS hS' := by
+    simp only [hS', ↓reduceDIte]
+    refine IsLUB.of_image (f := Subtype.val) (by simp) (isLUB_csSup' ?_)
+    exact (Subtype.mono_coe _).map_bddAbove hS'
+  csSup_of_not_bddAbove S hS := by simp [hS]
+  csSup_empty := by simp
+  sInf S := if hS : S.Nonempty then ⟨sInf ((↑) '' S), by
+    rcases hS with ⟨b, hb⟩
+    rw [mem_Iio]
+    apply b.2.trans_le'
+    apply csInf_le'
+    simpa using ⟨b.2, hb⟩⟩ else ⊥
+  isGLB_csInf S hS hS' := by
+    simp only [hS, ↓reduceDIte]
+    refine IsGLB.of_image (f := Subtype.val) (by simp) (isGLB_csInf ?_)
+    simpa
+  csInf_of_not_bddBelow := by simp
+
+lemma Set.Iio.coe_sSup [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)]
+    {S : Set (Iio a)} (hS : BddAbove S) : ↑(sSup S) = sSup ((↑) '' S : Set α) :=
+  congrArg Subtype.val (dif_pos hS)
+
+lemma Set.Iio.coe_sInf [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)]
+    {S : Set (Iio a)} (hS : S.Nonempty) : ↑(sInf S) = sInf ((↑) '' S : Set α) :=
+  congrArg Subtype.val (dif_pos hS)
+
+lemma Set.Iio.coe_iSup [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)]
+    {f : ι → Iio a} (hf : BddAbove (range f)) : ↑(iSup f) = (⨆ i, f i : α) :=
+  (coe_sSup hf).trans (congrArg sSup (range_comp Subtype.val f).symm)
+
+lemma Set.Iio.coe_iInf [ConditionallyCompleteLinearOrderBot α] {a : α} [Fact (¬ IsMin a)]
+    [Nonempty ι] {f : ι → Iio a} : ↑(iInf f) = (⨅ i, f i : α) :=
+  (coe_sInf (range_nonempty f)).trans (congrArg sInf (range_comp Subtype.val f).symm)
+
+end Iio
+
 section Icc
 
 open Classical in

Mathlib/Order/LatticeIntervals.lean

@@ -67,6 +67,26 @@ protected lemma coe_inf [SemilatticeInf α] {a : α} {x y : Iio a} :
     ↑(x ⊓ y) = (↑x ⊓ ↑y : α) :=
   rfl
 
+instance semilatticeSup [SemilatticeSup α] [IsLinearOrder α (· ≤ ·)] {a : α} :
+    SemilatticeSup (Iio a) :=
+  Subtype.semilatticeSup fun x y hx hy =>
+    (Std.Total.total x y).elim (fun h : x ≤ y => by rwa [sup_eq_right.2 h]) fun h => by
+      rwa [sup_eq_left.2 h]
+
+@[simp, norm_cast]
+protected lemma coe_sup [SemilatticeSup α] [IsLinearOrder α (· ≤ ·)] {a : α} {x y : Iio a} :
+    ↑(x ⊔ y) = (↑x ⊔ ↑y : α) :=
+  rfl
+
+instance [Lattice α] [IsLinearOrder α (· ≤ ·)] {a : α} : Lattice (Iio a) where
+
+instance orderBot [Preorder α] [OrderBot α] {a : α} [Fact (¬ IsMin a)] : OrderBot (Iio a) :=
+  (isLeast_Iio_bot Fact.out).orderBot
+
+@[simp, norm_cast]
+protected lemma coe_bot [Preorder α] [OrderBot α] (a : α) [Fact (¬ IsMin a)] :
+    (⊥ : Iio a) = (⊥ : α) := rfl
+
 end Iio
 
 namespace Ioc