feat: monotone function Cardinal → α is eventually constant (leanprover-community#37344)

Author: vihdzp

Mathlib.lean

@@ -7106,6 +7106,7 @@ public import Mathlib.SetTheory.Cardinal.Defs
 public import Mathlib.SetTheory.Cardinal.Divisibility
 public import Mathlib.SetTheory.Cardinal.ENat
 public import Mathlib.SetTheory.Cardinal.Embedding
+public import Mathlib.SetTheory.Cardinal.EventuallyConst
 public import Mathlib.SetTheory.Cardinal.Finite
 public import Mathlib.SetTheory.Cardinal.Finsupp
 public import Mathlib.SetTheory.Cardinal.Free

Mathlib/Logic/Small/Basic.lean

@@ -75,3 +75,5 @@ instance small_quot {α : Type u} [Small.{v} α] (r : α → α → Prop) : Smal
 
 instance small_quotient {α : Type u} [Small.{v} α] (s : Setoid α) : Small.{v} (Quotient s) :=
   small_of_surjective Quotient.mk_surjective
+
+instance small_orderDual {α : Type*} [h : Small.{v} α] : Small.{v} αᵒᵈ := h

Mathlib/Order/Preorder/Chain.lean

@@ -119,6 +119,14 @@ theorem Monotone.isChain_range [LinearOrder α] [Preorder β] {f : α → β} (h
   rw [← image_univ]
   exact hf.isChain_image (isChain_of_trichotomous _)
 
+lemma Antitone.isChain_image [Preorder α] [Preorder β] {s : Set α} {f : α → β}
+    (hf : Antitone f) (hs : IsChain (· ≤ ·) s) : IsChain (· ≤ ·) (f '' s) :=
+  hf.dual_left.isChain_image hs.symm
+
+theorem Antitone.isChain_range [LinearOrder α] [Preorder β] {f : α → β} (hf : Antitone f) :
+    IsChain (· ≤ ·) (range f) :=
+  hf.dual_left.isChain_range
+
 theorem IsChain.lt_of_le [PartialOrder α] {s : Set α} (h : IsChain (· ≤ ·) s) :
     IsChain (· < ·) s := fun _a ha _b hb hne ↦
   (h ha hb hne).imp hne.lt_of_le hne.lt_of_le'
@@ -222,6 +230,15 @@ theorem IsChain.exists3 (hchain : IsChain r s) [IsTrans α r] {a b c} (mem1 : a
 
 end Total
 
+/-- A chain in a partial order is a linear order. -/
+@[implicit_reducible]
+def IsChain.linearOrder [PartialOrder α] [DecidableLE α] {s : Set α} (hs : IsChain (· ≤ ·) s) :
+    LinearOrder s where
+  le_total := by
+    rintro ⟨a, ha⟩ ⟨b, hb⟩
+    exact hs.total ha hb
+  toDecidableLE x y := inferInstanceAs (Decidable (x.1 ≤ y.1))
+
 lemma IsChain.le_of_not_gt [Preorder α] (hs : IsChain (· ≤ ·) s)
     {x y : α} (hx : x ∈ s) (hy : y ∈ s) (h : ¬ x < y) : y ≤ x := by
   cases hs.total hx hy with

Mathlib/SetTheory/Cardinal/EventuallyConst.lean

@@ -0,0 +1,74 @@
+/-
+Copyright (c) 2026 Violeta Hernández Palacios. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Violeta Hernández Palacios
+-/
+module
+
+public import Mathlib.Order.Filter.EventuallyConst
+public import Mathlib.SetTheory.Cardinal.Aleph
+
+/-!
+# Eventually constant monotone functions
+
+This file proves variations of the following theorem: if `α` is a linear order and `β` is a partial
+order with `#β < cof α`, then any monotone function `f : α → β` must be eventually constant. In
+particular, this applies for functions from `Cardinal.{u}` or `Ordinal.{u}` into a `Small.{u}` type.
+-/
+
+public section
+
+universe u v
+
+variable {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β]
+
+open Cardinal Filter Order Set
+
+namespace Filter.EventuallyConst
+variable {f : α → β}
+
+theorem of_not_isCofinal_rangeSplitting [Nonempty α] (hf : Monotone f)
+    (hf' : ¬ IsCofinal (range (rangeSplitting f))) : atTop.EventuallyConst f := by
+  rw [eventuallyConst_atTop]
+  obtain ⟨i, hi⟩ := not_isCofinal_iff.1 hf'
+  refine ⟨i, fun j hij ↦ (hf hij).antisymm' <| (hf (hi _ ⟨⟨f j, j, rfl⟩, rfl⟩).le).trans' ?_⟩
+  rw [apply_rangeSplitting f]
+
+theorem of_monotone_of_lt_cof (hf : Monotone f) (hα : lift.{u} #β < lift.{v} (cof α)) :
+    atTop.EventuallyConst f := by
+  have : Nonempty α := by by_contra!; simp at hα
+  refine .of_not_isCofinal_rangeSplitting hf ?_
+  contrapose! hα
+  classical let := hf.isChain_range.linearOrder
+  rw [← lift_cof_congr_of_strictMono (rangeSplitting_strictMono hf) hα, lift_le]
+  exact (cof_le_cardinalMk _).trans (mk_set_le _)
+
+theorem of_antitone_of_lt_cof (hf : Antitone f) (hα : lift.{u} #β < lift.{v} (cof α)) :
+    atTop.EventuallyConst f :=
+  .of_monotone_of_lt_cof (β := βᵒᵈ) hf.dual_right hα
+
+end Filter.EventuallyConst
+
+namespace Cardinal
+variable {f : Cardinal.{v} → β} [Small.{v} β]
+
+theorem eventuallyConst_of_monotone (hf : Monotone f) : atTop.EventuallyConst f := by
+  refine .of_monotone_of_lt_cof hf ?_
+  simpa [← small_iff_lift_mk_lt_univ]
+
+theorem eventuallyConst_of_antitone (hf : Antitone f) : atTop.EventuallyConst f :=
+  eventuallyConst_of_monotone (β := βᵒᵈ) hf
+
+end Cardinal
+
+namespace Ordinal
+variable {f : Ordinal.{v} → β} [Small.{v} β]
+
+theorem eventuallyConst_of_monotone (hf : Monotone f) : atTop.EventuallyConst f := by
+  refine .of_monotone_of_lt_cof hf ?_
+  simpa [← small_iff_lift_mk_lt_univ]
+
+theorem eventuallyConst_of_antitone (hf : Antitone f) : atTop.EventuallyConst f :=
+  eventuallyConst_of_monotone (β := βᵒᵈ) hf
+
+end Ordinal