feat: monotone function Cardinal → α is eventually constant

Mathlib.lean

@@ -6828,6 +6828,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/SetTheory/Cardinal/EventuallyConst.lean

@@ -0,0 +1,54 @@
+/-
+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.Ordinal.Family
+
+/-!
+# Monotone functions from cardinals to small type are eventually constant
+
+We prove variations of the following theorem: if `α` is a `Small.{u}` partially ordered type, and
+`f : Cardinal.{u} → α` is a monotone function, then `f` is eventually constant.
+-/
+
+public section
+
+universe u
+
+variable {α : Type*} [PartialOrder α] [Small.{u} α]
+
+open Filter Set
+
+namespace Cardinal
+variable {f : Cardinal.{u} → α}
+
+theorem eventuallyConst_of_monotone (hf : Monotone f) : atTop.EventuallyConst f := by
+  rw [eventuallyConst_atTop]
+  obtain ⟨a, ha⟩ := bddAbove_of_small (range (rangeSplitting f))
+  refine ⟨a, fun b hb ↦ (hf hb).antisymm' ?_⟩
+  have := hf <| ha (mem_range_self ⟨f b, b, rfl⟩)
+  rwa [apply_rangeSplitting f] at this
+
+theorem eventuallyConst_of_antitone (hf : Antitone f) : atTop.EventuallyConst f :=
+  eventuallyConst_of_monotone (α := αᵒᵈ) hf
+
+end Cardinal
+
+namespace Ordinal
+variable {f : Ordinal.{u} → α}
+
+theorem eventuallyConst_of_monotone (hf : Monotone f) : atTop.EventuallyConst f := by
+  rw [eventuallyConst_atTop]
+  obtain ⟨a, ha⟩ := bddAbove_of_small (range (rangeSplitting f))
+  refine ⟨a, fun b hb ↦ (hf hb).antisymm' ?_⟩
+  have := hf <| ha (mem_range_self ⟨f b, b, rfl⟩)
+  rwa [apply_rangeSplitting f] at this
+
+theorem eventuallyConst_of_antitone (hf : Antitone f) : atTop.EventuallyConst f :=
+  eventuallyConst_of_monotone (α := αᵒᵈ) hf
+
+end Ordinal