feat: generalize NoMaxOrder to NoTopOrder (#24203)

Generalizes `NoMaxOrder` to `NoTopOrder` and `NoMinOrder` to `NoBotOrder` in some lemmas.

Author: plp127

Mathlib/Order/Bounds/Basic.lean

@@ -649,20 +649,25 @@ theorem isGLB_univ [OrderBot α] : IsGLB (univ : Set α) ⊥ :=
   isLeast_univ.isGLB
 
 @[simp]
-theorem NoMaxOrder.upperBounds_univ [NoMaxOrder α] : upperBounds (univ : Set α) = ∅ :=
+theorem NoTopOrder.upperBounds_univ [NoTopOrder α] : upperBounds (univ : Set α) = ∅ :=
   eq_empty_of_subset_empty fun b hb =>
-    let ⟨_, hx⟩ := exists_gt b
-    not_le_of_lt hx (hb trivial)
+    not_isTop b fun x => hb (mem_univ x)
+
+@[deprecated (since := "2025-04-18")]
+alias NoMaxOrder.upperBounds_univ := NoTopOrder.upperBounds_univ
 
 @[simp]
-theorem NoMinOrder.lowerBounds_univ [NoMinOrder α] : lowerBounds (univ : Set α) = ∅ :=
-  @NoMaxOrder.upperBounds_univ αᵒᵈ _ _
+theorem NoBotOrder.lowerBounds_univ [NoBotOrder α] : lowerBounds (univ : Set α) = ∅ :=
+  @NoTopOrder.upperBounds_univ αᵒᵈ _ _
+
+@[deprecated (since := "2025-04-18")]
+alias NoMinOrder.lowerBounds_univ := NoBotOrder.lowerBounds_univ
 
 @[simp]
-theorem not_bddAbove_univ [NoMaxOrder α] : ¬BddAbove (univ : Set α) := by simp [BddAbove]
+theorem not_bddAbove_univ [NoTopOrder α] : ¬BddAbove (univ : Set α) := by simp [BddAbove]
 
 @[simp]
-theorem not_bddBelow_univ [NoMinOrder α] : ¬BddBelow (univ : Set α) :=
+theorem not_bddBelow_univ [NoBotOrder α] : ¬BddBelow (univ : Set α) :=
   @not_bddAbove_univ αᵒᵈ _ _
 
 /-!
@@ -698,12 +703,11 @@ theorem isGLB_empty [OrderTop α] : IsGLB ∅ (⊤ : α) :=
 theorem isLUB_empty [OrderBot α] : IsLUB ∅ (⊥ : α) :=
   @isGLB_empty αᵒᵈ _ _
 
-theorem IsLUB.nonempty [NoMinOrder α] (hs : IsLUB s a) : s.Nonempty :=
-  let ⟨a', ha'⟩ := exists_lt a
+theorem IsLUB.nonempty [NoBotOrder α] (hs : IsLUB s a) : s.Nonempty :=
   nonempty_iff_ne_empty.2 fun h =>
-    not_le_of_lt ha' <| hs.right <| by rw [h, upperBounds_empty]; exact mem_univ _
+    not_isBot a fun _ => hs.right <| by rw [h, upperBounds_empty]; exact mem_univ _
 
-theorem IsGLB.nonempty [NoMaxOrder α] (hs : IsGLB s a) : s.Nonempty :=
+theorem IsGLB.nonempty [NoTopOrder α] (hs : IsGLB s a) : s.Nonempty :=
   hs.dual.nonempty
 
 theorem nonempty_of_not_bddAbove [ha : Nonempty α] (h : ¬BddAbove s) : s.Nonempty :=

Mathlib/Order/Filter/AtTopBot/Defs.lean

@@ -43,36 +43,38 @@ theorem mem_atTop [Preorder α] (a : α) : { b : α | a ≤ b } ∈ @atTop α _
 theorem Ici_mem_atTop [Preorder α] (a : α) : Ici a ∈ (atTop : Filter α) :=
   mem_atTop a
 
-theorem Ioi_mem_atTop [Preorder α] [NoMaxOrder α] (x : α) : Ioi x ∈ (atTop : Filter α) :=
-  let ⟨z, hz⟩ := exists_gt x
-  mem_of_superset (mem_atTop z) fun _ h => lt_of_lt_of_le hz h
+theorem Ioi_mem_atTop [Preorder α] [NoTopOrder α] (x : α) : Ioi x ∈ (atTop : Filter α) :=
+  let ⟨z, hz⟩ := exists_not_le x
+  mem_of_superset (inter_mem (mem_atTop x) (mem_atTop z))
+    fun _ ⟨hxy, hzy⟩ => lt_of_le_not_le hxy fun hyx => hz (hzy.trans hyx)
 
 theorem mem_atBot [Preorder α] (a : α) : { b : α | b ≤ a } ∈ @atBot α _ :=
   mem_iInf_of_mem a <| Subset.refl _
 
 theorem Iic_mem_atBot [Preorder α] (a : α) : Iic a ∈ (atBot : Filter α) :=
   mem_atBot a
 
-theorem Iio_mem_atBot [Preorder α] [NoMinOrder α] (x : α) : Iio x ∈ (atBot : Filter α) :=
-  let ⟨z, hz⟩ := exists_lt x
-  mem_of_superset (mem_atBot z) fun _ h => lt_of_le_of_lt h hz
+theorem Iio_mem_atBot [Preorder α] [NoBotOrder α] (x : α) : Iio x ∈ (atBot : Filter α) :=
+  let ⟨z, hz⟩ := exists_not_ge x
+  mem_of_superset (inter_mem (mem_atBot x) (mem_atBot z))
+    fun _ ⟨hyx, hyz⟩ => lt_of_le_not_le hyx fun hxy => hz (hxy.trans hyz)
 
 theorem eventually_ge_atTop [Preorder α] (a : α) : ∀ᶠ x in atTop, a ≤ x :=
   mem_atTop a
 
 theorem eventually_le_atBot [Preorder α] (a : α) : ∀ᶠ x in atBot, x ≤ a :=
   mem_atBot a
 
-theorem eventually_gt_atTop [Preorder α] [NoMaxOrder α] (a : α) : ∀ᶠ x in atTop, a < x :=
+theorem eventually_gt_atTop [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, a < x :=
   Ioi_mem_atTop a
 
-theorem eventually_ne_atTop [Preorder α] [NoMaxOrder α] (a : α) : ∀ᶠ x in atTop, x ≠ a :=
+theorem eventually_ne_atTop [Preorder α] [NoTopOrder α] (a : α) : ∀ᶠ x in atTop, x ≠ a :=
   (eventually_gt_atTop a).mono fun _ => ne_of_gt
 
-theorem eventually_lt_atBot [Preorder α] [NoMinOrder α] (a : α) : ∀ᶠ x in atBot, x < a :=
+theorem eventually_lt_atBot [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x < a :=
   Iio_mem_atBot a
 
-theorem eventually_ne_atBot [Preorder α] [NoMinOrder α] (a : α) : ∀ᶠ x in atBot, x ≠ a :=
+theorem eventually_ne_atBot [Preorder α] [NoBotOrder α] (a : α) : ∀ᶠ x in atBot, x ≠ a :=
   (eventually_lt_atBot a).mono fun _ => ne_of_lt
 
 theorem _root_.IsTop.atTop_eq [Preorder α] {a : α} (ha : IsTop a) : atTop = 𝓟 (Ici a) :=

Mathlib/Order/Filter/AtTopBot/Disjoint.lean

@@ -24,20 +24,20 @@ theorem disjoint_atBot_principal_Ioi [Preorder α] (x : α) : Disjoint atBot (
 theorem disjoint_atTop_principal_Iio [Preorder α] (x : α) : Disjoint atTop (𝓟 (Iio x)) :=
   @disjoint_atBot_principal_Ioi αᵒᵈ _ _
 
-theorem disjoint_atTop_principal_Iic [Preorder α] [NoMaxOrder α] (x : α) :
+theorem disjoint_atTop_principal_Iic [Preorder α] [NoTopOrder α] (x : α) :
     Disjoint atTop (𝓟 (Iic x)) :=
   disjoint_of_disjoint_of_mem (Iic_disjoint_Ioi le_rfl).symm (Ioi_mem_atTop x)
     (mem_principal_self _)
 
-theorem disjoint_atBot_principal_Ici [Preorder α] [NoMinOrder α] (x : α) :
+theorem disjoint_atBot_principal_Ici [Preorder α] [NoBotOrder α] (x : α) :
     Disjoint atBot (𝓟 (Ici x)) :=
   @disjoint_atTop_principal_Iic αᵒᵈ _ _ _
 
-theorem disjoint_pure_atTop [Preorder α] [NoMaxOrder α] (x : α) : Disjoint (pure x) atTop :=
+theorem disjoint_pure_atTop [Preorder α] [NoTopOrder α] (x : α) : Disjoint (pure x) atTop :=
   Disjoint.symm <| (disjoint_atTop_principal_Iic x).mono_right <| le_principal_iff.2 <|
     mem_pure.2 right_mem_Iic
 
-theorem disjoint_pure_atBot [Preorder α] [NoMinOrder α] (x : α) : Disjoint (pure x) atBot :=
+theorem disjoint_pure_atBot [Preorder α] [NoBotOrder α] (x : α) : Disjoint (pure x) atBot :=
   @disjoint_pure_atTop αᵒᵈ _ _ _
 
 theorem disjoint_atBot_atTop [PartialOrder α] [Nontrivial α] :

Mathlib/Order/Filter/AtTopBot/Tendsto.lean

@@ -21,39 +21,39 @@ open Set
 
 namespace Filter
 
-theorem not_tendsto_const_atTop [Preorder α] [NoMaxOrder α] (x : α) (l : Filter β) [l.NeBot] :
+theorem not_tendsto_const_atTop [Preorder α] [NoTopOrder α] (x : α) (l : Filter β) [l.NeBot] :
     ¬Tendsto (fun _ => x) l atTop :=
   tendsto_const_pure.not_tendsto (disjoint_pure_atTop x)
 
-theorem not_tendsto_const_atBot [Preorder α] [NoMinOrder α] (x : α) (l : Filter β) [l.NeBot] :
+theorem not_tendsto_const_atBot [Preorder α] [NoBotOrder α] (x : α) (l : Filter β) [l.NeBot] :
     ¬Tendsto (fun _ => x) l atBot :=
   tendsto_const_pure.not_tendsto (disjoint_pure_atBot x)
 
-protected theorem Tendsto.eventually_gt_atTop [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α}
+protected theorem Tendsto.eventually_gt_atTop [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α}
     (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, c < f x :=
   hf.eventually (eventually_gt_atTop c)
 
 protected theorem Tendsto.eventually_ge_atTop [Preorder β] {f : α → β} {l : Filter α}
     (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, c ≤ f x :=
   hf.eventually (eventually_ge_atTop c)
 
-protected theorem Tendsto.eventually_ne_atTop [Preorder β] [NoMaxOrder β] {f : α → β} {l : Filter α}
+protected theorem Tendsto.eventually_ne_atTop [Preorder β] [NoTopOrder β] {f : α → β} {l : Filter α}
     (hf : Tendsto f l atTop) (c : β) : ∀ᶠ x in l, f x ≠ c :=
   hf.eventually (eventually_ne_atTop c)
 
-protected theorem Tendsto.eventually_ne_atTop' [Preorder β] [NoMaxOrder β] {f : α → β}
+protected theorem Tendsto.eventually_ne_atTop' [Preorder β] [NoTopOrder β] {f : α → β}
     {l : Filter α} (hf : Tendsto f l atTop) (c : α) : ∀ᶠ x in l, x ≠ c :=
   (hf.eventually_ne_atTop (f c)).mono fun _ => ne_of_apply_ne f
 
-protected theorem Tendsto.eventually_lt_atBot [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α}
+protected theorem Tendsto.eventually_lt_atBot [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α}
     (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x < c :=
   hf.eventually (eventually_lt_atBot c)
 
 protected theorem Tendsto.eventually_le_atBot [Preorder β] {f : α → β} {l : Filter α}
     (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x ≤ c :=
   hf.eventually (eventually_le_atBot c)
 
-protected theorem Tendsto.eventually_ne_atBot [Preorder β] [NoMinOrder β] {f : α → β} {l : Filter α}
+protected theorem Tendsto.eventually_ne_atBot [Preorder β] [NoBotOrder β] {f : α → β} {l : Filter α}
     (hf : Tendsto f l atBot) (c : β) : ∀ᶠ x in l, f x ≠ c :=
   hf.eventually (eventually_ne_atBot c)
 

Mathlib/Order/Filter/Cofinite.lean

@@ -100,10 +100,14 @@ theorem le_cofinite_iff_compl_singleton_mem : l ≤ cofinite ↔ ∀ x, {x}ᶜ 
 theorem le_cofinite_iff_eventually_ne : l ≤ cofinite ↔ ∀ x, ∀ᶠ y in l, y ≠ x :=
   le_cofinite_iff_compl_singleton_mem
 
-/-- If `α` is a preorder with no maximal element, then `atTop ≤ cofinite`. -/
-theorem atTop_le_cofinite [Preorder α] [NoMaxOrder α] : (atTop : Filter α) ≤ cofinite :=
+/-- If `α` is a preorder with no top element, then `atTop ≤ cofinite`. -/
+theorem atTop_le_cofinite [Preorder α] [NoTopOrder α] : (atTop : Filter α) ≤ cofinite :=
   le_cofinite_iff_eventually_ne.mpr eventually_ne_atTop
 
+/-- If `α` is a preorder with no bottom element, then `atBot ≤ cofinite`. -/
+theorem atBot_le_cofinite [Preorder α] [NoBotOrder α] : (atBot : Filter α) ≤ cofinite :=
+  le_cofinite_iff_eventually_ne.mpr eventually_ne_atBot
+
 theorem comap_cofinite_le (f : α → β) : comap f cofinite ≤ cofinite :=
   le_cofinite_iff_eventually_ne.mpr fun x =>
     mem_comap.2 ⟨{f x}ᶜ, (finite_singleton _).compl_mem_cofinite, fun _ => ne_of_apply_ne f⟩

Mathlib/Order/WithBot.lean

@@ -330,23 +330,23 @@ theorem lt_coe_bot [OrderBot α] : x < (⊥ : α) ↔ x = ⊥ := by cases x <;>
 lemma eq_bot_iff_forall_lt : x = ⊥ ↔ ∀ b : α, x < b := by
   cases x <;> simp; simpa using ⟨_, lt_irrefl _⟩
 
-lemma eq_bot_iff_forall_le [NoMinOrder α] : x = ⊥ ↔ ∀ b : α, x ≤ b := by
-  refine ⟨by simp +contextual, fun h ↦ eq_bot_iff_forall_lt.2 fun y ↦ ?_⟩
-  obtain ⟨w, hw⟩ := exists_lt y
-  exact (h w).trans_lt (coe_lt_coe.2 hw)
+lemma eq_bot_iff_forall_le [NoBotOrder α] : x = ⊥ ↔ ∀ b : α, x ≤ b := by
+  refine ⟨by simp +contextual, fun h ↦ (x.eq_bot_iff_forall_ne).2 fun y => ?_⟩
+  rintro rfl
+  exact not_isBot y fun z => coe_le_coe.1 (h z)
 
 @[deprecated (since := "2025-03-19")] alias forall_lt_iff_eq_bot := eq_bot_iff_forall_lt
 @[deprecated (since := "2025-03-19")] alias forall_le_iff_eq_bot := eq_bot_iff_forall_le
 
-lemma forall_le_coe_iff_le [NoMinOrder α] : (∀ a : α, y ≤ a → x ≤ a) ↔ x ≤ y := by
+lemma forall_le_coe_iff_le [NoBotOrder α] : (∀ a : α, y ≤ a → x ≤ a) ↔ x ≤ y := by
   obtain _ | y := y
   · simp [WithBot.none_eq_bot, eq_bot_iff_forall_le]
   · exact ⟨fun h ↦ h _ le_rfl, fun hmn a ham ↦ hmn.trans ham⟩
 
 end Preorder
 
 section PartialOrder
-variable [PartialOrder α] [NoMinOrder α] {x y : WithBot α}
+variable [PartialOrder α] [NoBotOrder α] {x y : WithBot α}
 
 lemma eq_of_forall_le_coe_iff (h : ∀ a : α, x ≤ a ↔ y ≤ a) : x = y :=
   le_antisymm (forall_le_coe_iff_le.mp fun a ↦ (h a).2) (forall_le_coe_iff_le.mp fun a ↦ (h a).1)
@@ -829,19 +829,19 @@ theorem coe_top_lt [OrderTop α] : (⊤ : α) < x ↔ x = ⊤ := by cases x <;>
 lemma eq_top_iff_forall_gt : y = ⊤ ↔ ∀ a : α, a < y := by
   cases y <;> simp; simpa using ⟨_, lt_irrefl _⟩
 
-lemma eq_top_iff_forall_ge [NoMaxOrder α] : y = ⊤ ↔ ∀ a : α, a ≤ y :=
+lemma eq_top_iff_forall_ge [NoTopOrder α] : y = ⊤ ↔ ∀ a : α, a ≤ y :=
   WithBot.eq_bot_iff_forall_le (α := αᵒᵈ)
 
 @[deprecated (since := "2025-03-19")] alias forall_gt_iff_eq_top := eq_top_iff_forall_gt
 @[deprecated (since := "2025-03-19")] alias forall_ge_iff_eq_top := eq_top_iff_forall_ge
 
-lemma forall_coe_le_iff_le [NoMaxOrder α] : (∀ a : α, a ≤ x → a ≤ y) ↔ x ≤ y :=
+lemma forall_coe_le_iff_le [NoTopOrder α] : (∀ a : α, a ≤ x → a ≤ y) ↔ x ≤ y :=
   WithBot.forall_le_coe_iff_le (α := αᵒᵈ)
 
 end Preorder
 
 section PartialOrder
-variable [PartialOrder α] [NoMaxOrder α] {x y : WithTop α}
+variable [PartialOrder α] [NoTopOrder α] {x y : WithTop α}
 
 lemma eq_of_forall_coe_le_iff (h : ∀ a : α, a ≤ x ↔ a ≤ y) : x = y :=
   WithBot.eq_of_forall_le_coe_iff (α := αᵒᵈ) h
@@ -973,7 +973,7 @@ end WithTop
 
 section WithBotWithTop
 
-lemma WithBot.eq_top_iff_forall_ge [Preorder α] [Nonempty α] [NoMaxOrder α]
+lemma WithBot.eq_top_iff_forall_ge [Preorder α] [Nonempty α] [NoTopOrder α]
     {x : WithBot (WithTop α)} : x = ⊤ ↔ ∀ a : α, a ≤ x := by
   refine ⟨by aesop, fun H ↦ ?_⟩
   induction x