feat: use junk value in the definition of conditionally complete linear order (#6571)

Currently, in a conditionally complete linear order, the supremum of an unbounded set hasn't any specific property. However, in all instances in mathlib, all unbounded sets have the same supremum. This PR adds this requirement in mathlib. This will be convenient to remove boundedness assumptions in measurability statements.

Author: sgouezel

Mathlib/Algebra/Tropical/Lattice.lean

@@ -72,4 +72,20 @@ instance instConditionallyCompleteLatticeTropical [ConditionallyCompleteLattice
       csInf_le (untrop_monotone.map_bddBelow hs) (Set.mem_image_of_mem untrop hx) }
 
 instance [ConditionallyCompleteLinearOrder R] : ConditionallyCompleteLinearOrder (Tropical R) :=
-  { instConditionallyCompleteLatticeTropical, Tropical.instLinearOrderTropical with }
+  { instConditionallyCompleteLatticeTropical, Tropical.instLinearOrderTropical with
+    csSup_of_not_bddAbove := by
+      intro s hs
+      have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
+      simp [sSup, this]
+      apply csSup_of_not_bddAbove
+      contrapose! hs
+      change BddAbove (tropOrderIso.symm '' s) at hs
+      exact tropOrderIso.symm.bddAbove_image.1 hs
+    csInf_of_not_bddBelow := by
+      intro s hs
+      have : Set.range untrop = (Set.univ : Set R) := Equiv.range_eq_univ tropEquiv.symm
+      simp [sInf, this]
+      apply csInf_of_not_bddBelow
+      contrapose! hs
+      change BddBelow (tropOrderIso.symm '' s) at hs
+      exact tropOrderIso.symm.bddBelow_image.1 hs }

Mathlib/Data/Int/ConditionallyCompleteOrder.lean

@@ -55,7 +55,9 @@ instance : ConditionallyCompleteLinearOrder ℤ :=
       have : s.Nonempty ∧ BddBelow s := ⟨hs, ⟨n, hns⟩⟩
       -- Porting note: this was `rw [dif_pos this]`
       simp only [this, and_self, dite_true, ge_iff_le]
-      exact hns (leastOfBdd _ (Classical.choose_spec this.2) _).2.1 }
+      exact hns (leastOfBdd _ (Classical.choose_spec this.2) _).2.1
+    csSup_of_not_bddAbove := fun s hs ↦ by simp [hs]
+    csInf_of_not_bddBelow := fun s hs ↦ by simp [hs] }
 
 namespace Int
 

Mathlib/Data/Nat/Lattice.lean

@@ -132,7 +132,15 @@ noncomputable instance : ConditionallyCompleteLinearOrderBot ℕ :=
       simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
         not_false_iff, exists_const]
       apply bot_unique (Nat.find_min' _ _)
-      trivial }
+      trivial
+    csSup_of_not_bddAbove := by
+      intro s hs
+      simp only [mem_univ, forall_true_left, sSup]
+      rw [dif_neg, dif_neg]
+      · simp only [not_exists, not_forall, not_le]
+        exact fun n ↦ ⟨n+1, lt.base n⟩
+      · exact hs
+    csInf_of_not_bddBelow := fun s hs ↦ by simp at hs }
 
 theorem sSup_mem {s : Set ℕ} (h₁ : s.Nonempty) (h₂ : BddAbove s) : sSup s ∈ s :=
   let ⟨k, hk⟩ := h₂

Mathlib/Data/Real/Basic.lean

@@ -761,7 +761,9 @@ noncomputable instance : ConditionallyCompleteLinearOrder ℝ :=
     le_csSup := fun s a hs ha => (Real.isLUB_sSup s ⟨a, ha⟩ hs).1 ha
     csSup_le := fun s a hs ha => (Real.isLUB_sSup s hs ⟨a, ha⟩).2 ha
     csInf_le := fun s a hs ha => (Real.is_glb_sInf s ⟨a, ha⟩ hs).1 ha
-    le_csInf := fun s a hs ha => (Real.is_glb_sInf s hs ⟨a, ha⟩).2 ha }
+    le_csInf := fun s a hs ha => (Real.is_glb_sInf s hs ⟨a, ha⟩).2 ha
+    csSup_of_not_bddAbove := fun s hs ↦ by simp [hs, sSup_def]
+    csInf_of_not_bddBelow := fun s hs ↦ by simp [hs, sInf_def, sSup_def] }
 
 theorem lt_sInf_add_pos {s : Set ℝ} (h : s.Nonempty) {ε : ℝ} (hε : 0 < ε) :
     ∃ a ∈ s, a < sInf s + ε :=

Mathlib/Order/CompleteLatticeIntervals.lean

@@ -96,6 +96,40 @@ attribute [local instance] subsetSupSet
 
 attribute [local instance] subsetInfSet
 
+lemma sSup_subtype_eq_sSup_univ_of_not_bddAbove {s : Set α} [Inhabited s]
+    (t : Set s) (ht : ¬BddAbove t) : sSup t = sSup univ := by
+  have A : ∀ (u : Set s), ¬BddAbove u → BddAbove (Subtype.val '' u) →
+      sSup ((↑) '' u : Set α) ∉ s := by
+    intro u hu Hu
+    contrapose! hu
+    refine ⟨⟨_, hu⟩, ?_⟩
+    rintro ⟨x, xs⟩ hx
+    simp only [Subtype.mk_le_mk]
+    apply le_csSup Hu
+    exact ⟨⟨x, xs⟩, hx, rfl⟩
+  by_cases Ht : BddAbove ((↑) '' t : Set α)
+  · have I1 : sSup ((↑) '' t : Set α) ∉ s := A t ht Ht
+    have I2 : sSup ((↑) '' (univ : Set s) : Set α) ∉ s := by
+      apply A
+      · contrapose! ht; exact ht.mono (subset_univ _)
+      · refine ⟨sSup ((↑) '' t : Set α), ?_⟩
+        rintro - ⟨⟨x, hx⟩, -, rfl⟩
+        simp [BddAbove, not_nonempty_iff_eq_empty] at ht
+        have : ⟨x, hx⟩ ∉ upperBounds t := by simp [ht]
+        obtain ⟨⟨y, ys⟩, yt, hy⟩ : ∃ y, y ∈ t ∧ { val := x, property := hx } < y :=
+          by simpa only [Subtype.mk_le_mk, not_forall, not_le, exists_prop, exists_and_right,
+            mem_upperBounds]
+        refine le_trans (le_of_lt hy) ?_
+        exact le_csSup Ht ⟨⟨y, ys⟩, yt, rfl⟩
+    simp only [sSup, I1, I2, dite_false]
+  · have I : ¬BddAbove ((↑) '' (univ : Set s) : Set α) := by
+      contrapose! Ht; exact Ht.mono (image_subset Subtype.val (subset_univ _))
+    have X : sSup ((↑) '' t : Set α) = sSup (univ : Set α) :=
+      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ Ht
+    have Y : sSup ((↑) '' (univ : Set s) : Set α) = sSup (univ : Set α) :=
+      ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ I
+    simp only [sSup, X, Y]
+
 /-- For a nonempty subset of a conditionally complete linear order to be a conditionally complete
 linear order, it suffices that it contain the `sSup` of all its nonempty bounded-above subsets, and
 the `sInf` of all its nonempty bounded-below subsets.
@@ -124,7 +158,9 @@ noncomputable def subsetConditionallyCompleteLinearOrder [Inhabited s]
     csInf_le := by
       rintro t c h_bdd hct
       rw [← Subtype.coe_le_coe, ← subset_sInf_of_within s (h_Inf ⟨c, hct⟩ h_bdd)]
-      exact (Subtype.mono_coe s).csInf_image_le hct h_bdd }
+      exact (Subtype.mono_coe s).csInf_image_le hct h_bdd
+    csSup_of_not_bddAbove := sSup_subtype_eq_sSup_univ_of_not_bddAbove
+    csInf_of_not_bddBelow := @sSup_subtype_eq_sSup_univ_of_not_bddAbove αᵒᵈ _ _ _ }
 #align subset_conditionally_complete_linear_order subsetConditionallyCompleteLinearOrder
 
 section OrdConnected

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -201,6 +201,10 @@ class ConditionallyCompleteLinearOrder (α : Type*) extends ConditionallyComplet
   /-- In a `ConditionallyCompleteLinearOrder`, we assume the order relations are all decidable. -/
   decidableLT : DecidableRel (· < · : α → α → Prop) :=
     @decidableLTOfDecidableLE _ _ decidableLE
+  /-- If a set is not bounded above, its supremum is by convention `Sup univ`. -/
+  csSup_of_not_bddAbove : ∀ s, ¬BddAbove s → sSup s = sSup (univ : Set α)
+  /-- If a set is not bounded below, its infimum is by convention `Inf univ`. -/
+  csInf_of_not_bddBelow : ∀ s, ¬BddBelow s → sInf s = sInf (univ : Set α)
 #align conditionally_complete_linear_order ConditionallyCompleteLinearOrder
 
 instance (α : Type*) [ConditionallyCompleteLinearOrder α] : LinearOrder α :=
@@ -256,7 +260,10 @@ instance (priority := 100) CompleteLattice.toConditionallyCompleteLattice [Compl
 -- see Note [lower instance priority]
 instance (priority := 100) CompleteLinearOrder.toConditionallyCompleteLinearOrderBot {α : Type*}
     [h : CompleteLinearOrder α] : ConditionallyCompleteLinearOrderBot α :=
-  { CompleteLattice.toConditionallyCompleteLattice, h with csSup_empty := sSup_empty }
+  { CompleteLattice.toConditionallyCompleteLattice, h with
+    csSup_empty := sSup_empty
+    csSup_of_not_bddAbove := fun s H ↦ (H (OrderTop.bddAbove s)).elim
+    csInf_of_not_bddBelow := fun s H ↦ (H (OrderBot.bddBelow s)).elim }
 #align complete_linear_order.to_conditionally_complete_linear_order_bot CompleteLinearOrder.toConditionallyCompleteLinearOrderBot
 
 section
@@ -285,7 +292,15 @@ noncomputable def IsWellOrder.conditionallyCompleteLinearOrderBot (α : Type*)
       have h's : (upperBounds s).Nonempty := ⟨a, has⟩
       simp only [h's, dif_pos]
       simpa using h.wf.not_lt_min _ h's has
-    csSup_empty := by simpa using eq_bot_iff.2 (not_lt.1 <| h.wf.not_lt_min _ _ <| mem_univ ⊥) }
+    csSup_empty := by simpa using eq_bot_iff.2 (not_lt.1 <| h.wf.not_lt_min _ _ <| mem_univ ⊥)
+    csSup_of_not_bddAbove := by
+      intro s H
+      have A : ¬(BddAbove (univ : Set α)) := by
+        contrapose! H; exact H.mono (subset_univ _)
+      have B : ¬((upperBounds s).Nonempty) := H
+      have C : ¬((upperBounds (univ : Set α)).Nonempty) := A
+      simp [sSup, B, C]
+    csInf_of_not_bddBelow := fun s H ↦ (H (OrderBot.bddBelow s)).elim }
 #align is_well_order.conditionally_complete_linear_order_bot IsWellOrder.conditionallyCompleteLinearOrderBot
 
 end
@@ -301,7 +316,9 @@ instance instConditionallyCompleteLatticeOrderDual (α : Type*) [ConditionallyCo
     csInf_le := @ConditionallyCompleteLattice.le_csSup α _ }
 
 instance (α : Type*) [ConditionallyCompleteLinearOrder α] : ConditionallyCompleteLinearOrder αᵒᵈ :=
-  { instConditionallyCompleteLatticeOrderDual α, OrderDual.instLinearOrder α with }
+  { instConditionallyCompleteLatticeOrderDual α, OrderDual.instLinearOrder α with
+    csSup_of_not_bddAbove := @ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow α _
+    csInf_of_not_bddBelow := @ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove α _ }
 
 end OrderDual
 
@@ -961,6 +978,52 @@ theorem exists_lt_of_ciInf_lt [Nonempty ι] {f : ι → α} (h : iInf f < a) : 
   @exists_lt_of_lt_ciSup αᵒᵈ _ _ _ _ _ h
 #align exists_lt_of_cinfi_lt exists_lt_of_ciInf_lt
 
+theorem csSup_of_not_bddAbove {s : Set α} (hs : ¬BddAbove s) : sSup s = sSup univ :=
+  ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove s hs
+
+theorem csInf_of_not_bddBelow {s : Set α} (hs : ¬BddBelow s) : sInf s = sInf univ :=
+  ConditionallyCompleteLinearOrder.csInf_of_not_bddBelow s hs
+
+/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
+`s` and `t` have the same supremum. This holds even when the sets may be empty or unbounded. -/
+theorem csSup_eq_csSup_of_forall_exists_le {s t : Set α}
+    (hs : ∀ x ∈ s, ∃ y ∈ t, x ≤ y) (ht : ∀ y ∈ t, ∃ x ∈ s, y ≤ x) :
+    sSup s = sSup t := by
+  rcases eq_empty_or_nonempty s with rfl|s_ne
+  · have : t = ∅ := eq_empty_of_forall_not_mem (fun y yt ↦ by simpa using ht y yt)
+    rw [this]
+  rcases eq_empty_or_nonempty t with rfl|t_ne
+  · have : s = ∅ := eq_empty_of_forall_not_mem (fun x xs ↦ by simpa using hs x xs)
+    rw [this]
+  by_cases B : BddAbove s ∨ BddAbove t
+  · have Bs : BddAbove s := by
+      rcases B with hB|⟨b, hb⟩
+      · exact hB
+      · refine ⟨b, fun x hx ↦ ?_⟩
+        rcases hs x hx with ⟨y, hy, hxy⟩
+        exact hxy.trans (hb hy)
+    have Bt : BddAbove t := by
+      rcases B with ⟨b, hb⟩|hB
+      · refine ⟨b, fun y hy ↦ ?_⟩
+        rcases ht y hy with ⟨x, hx, hyx⟩
+        exact hyx.trans (hb hx)
+      · exact hB
+    apply le_antisymm
+    · apply csSup_le s_ne (fun x hx ↦ ?_)
+      rcases hs x hx with ⟨y, yt, hxy⟩
+      exact hxy.trans (le_csSup Bt yt)
+    · apply csSup_le t_ne (fun y hy ↦ ?_)
+      rcases ht y hy with ⟨x, xs, hyx⟩
+      exact hyx.trans (le_csSup Bs xs)
+  · simp [csSup_of_not_bddAbove, (not_or.1 B).1, (not_or.1 B).2]
+
+/-- When every element of a set `s` is bounded by an element of a set `t`, and conversely, then
+`s` and `t` have the same supremum. This holds even when the sets may be empty or unbounded. -/
+theorem csInf_eq_csInf_of_forall_exists_le {s t : Set α}
+    (hs : ∀ x ∈ s, ∃ y ∈ t, y ≤ x) (ht : ∀ y ∈ t, ∃ x ∈ s, x ≤ y) :
+    sInf s = sInf t :=
+  @csSup_eq_csSup_of_forall_exists_le αᵒᵈ _ s t hs ht
+
 open Function
 
 variable [IsWellOrder α (· < ·)]