feat: The range in a succ order is unbounded (#6883)

Strictly monotone/antitone functions from an order without top/bottom to a succ/pred order have unbounded range.

Mathlib/Order/Max.lean

@@ -75,6 +75,9 @@ instance nonempty_lt [LT α] [NoMinOrder α] (a : α) : Nonempty { x // x < a }
 instance nonempty_gt [LT α] [NoMaxOrder α] (a : α) : Nonempty { x // a < x } :=
   nonempty_subtype.2 (exists_gt a)
 
+instance IsEmpty.toNoMaxOrder [LT α] [IsEmpty α] : NoMaxOrder α := ⟨isEmptyElim⟩
+instance IsEmpty.toNoMinOrder [LT α] [IsEmpty α] : NoMinOrder α := ⟨isEmptyElim⟩
+
 instance OrderDual.noBotOrder [LE α] [NoTopOrder α] : NoBotOrder αᵒᵈ :=
   ⟨fun a => @exists_not_le α _ _ a⟩
 #align order_dual.no_bot_order OrderDual.noBotOrder

Mathlib/Order/SuccPred/Basic.lean

@@ -56,7 +56,7 @@ class SuccPredOrder (α : Type*) [Preorder α] extends SuccOrder α, PredOrder 
 
 open Function OrderDual Set
 
-variable {α : Type*}
+variable {α β : Type*}
 
 /-- Order equipped with a sensible successor function. -/
 @[ext]
@@ -255,6 +255,9 @@ theorem succ_le_iff_of_not_isMax (ha : ¬IsMax a) : succ a ≤ b ↔ a < b :=
   ⟨(lt_succ_of_not_isMax ha).trans_le, succ_le_of_lt⟩
 #align order.succ_le_iff_of_not_is_max Order.succ_le_iff_of_not_isMax
 
+lemma succ_lt_succ_of_not_isMax (h : a < b) (hb : ¬ IsMax b) : succ a < succ b :=
+(lt_succ_iff_of_not_isMax hb).2 $ succ_le_of_lt h
+
 theorem succ_lt_succ_iff_of_not_isMax (ha : ¬IsMax a) (hb : ¬IsMax b) : succ a < succ b ↔ a < b :=
   by rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]
 #align order.succ_lt_succ_iff_of_not_is_max Order.succ_lt_succ_iff_of_not_isMax
@@ -638,6 +641,9 @@ theorem le_pred_iff_of_not_isMin (ha : ¬IsMin a) : b ≤ pred a ↔ b < a :=
   ⟨fun h => h.trans_lt <| pred_lt_of_not_isMin ha, le_pred_of_lt⟩
 #align order.le_pred_iff_of_not_is_min Order.le_pred_iff_of_not_isMin
 
+lemma pred_lt_pred_of_not_isMin (h : a < b) (ha : ¬ IsMin a) : pred a < pred b :=
+(pred_lt_iff_of_not_isMin ha).2 $ le_pred_of_lt h
+
 @[simp, mono]
 theorem pred_le_pred {a b : α} (h : a ≤ b) : pred a ≤ pred b :=
   succ_le_succ h.dual
@@ -1463,6 +1469,34 @@ end PredOrder
 
 end LinearOrder
 
+section bdd_range
+variable [Preorder α] [Nonempty α] [Preorder β] {f : α → β}
+
+lemma StrictMono.not_bddAbove_range [NoMaxOrder α] [SuccOrder β] [IsSuccArchimedean β]
+  (hf : StrictMono f) : ¬ BddAbove (Set.range f) := by
+  rintro ⟨m, hm⟩
+  have hm' : ∀ a, f a ≤ m := λ a ↦ hm $ Set.mem_range_self _
+  obtain ⟨a₀⟩ := ‹Nonempty α›
+  suffices : ∀ b, f a₀ ≤ b → ∃ a, b < f a
+  { obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
+    exact ha.not_le (hm' a) }
+  have h : ∀ a, ∃ a', f a < f a' := λ a ↦ (exists_gt a).imp (λ a' h ↦ hf h)
+  apply Succ.rec
+  { exact h a₀ }
+  rintro b _ ⟨a, hba⟩
+  exact (h a).imp (λ a' ↦ (succ_le_of_lt hba).trans_lt)
+
+lemma StrictMono.not_bddBelow_range [NoMinOrder α] [PredOrder β] [IsPredArchimedean β]
+  (hf : StrictMono f) : ¬ BddBelow (Set.range f) := hf.dual.not_bddAbove_range
+
+lemma StrictAnti.not_bddAbove_range [NoMinOrder α] [SuccOrder β] [IsSuccArchimedean β]
+  (hf : StrictAnti f) : ¬ BddAbove (Set.range f) := hf.dual_right.not_bddBelow_range
+
+lemma StrictAnti.not_bddBelow_range [NoMaxOrder α] [PredOrder β] [IsPredArchimedean β]
+  (hf : StrictAnti f) : ¬ BddBelow (Set.range f) := hf.dual_right.not_bddAbove_range
+
+end bdd_range
+
 section IsWellOrder
 
 variable [LinearOrder α]