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.

theorem Filter.EventuallyConst.of_not_isCofinal_rangeSplitting {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} [Nonempty α] (hf : Monotone f) (hf' : ¬IsCofinal (Set.range (Set.rangeSplitting f))) : EventuallyConst f atTop

theorem Filter.EventuallyConst.of_monotone_of_lt_cof {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} (hf : Monotone f) (hα : Cardinal.lift.{u, v} (Cardinal.mk β) < Cardinal.lift.{v, u} (Order.cof α)) : EventuallyConst f atTop

theorem Filter.EventuallyConst.of_antitone_of_lt_cof {α : Type u} {β : Type v} [LinearOrder α] [PartialOrder β] {f : α → β} (hf : Antitone f) (hα : Cardinal.lift.{u, v} (Cardinal.mk β) < Cardinal.lift.{v, u} (Order.cof α)) : EventuallyConst f atTop

theorem Cardinal.eventuallyConst_of_monotone {β : Type v} [PartialOrder β] {f : Cardinal.{v} → β} [Small.{v, v} β] (hf : Monotone f) : Filter.EventuallyConst f Filter.atTop

theorem Cardinal.eventuallyConst_of_antitone {β : Type v} [PartialOrder β] {f : Cardinal.{v} → β} [Small.{v, v} β] (hf : Antitone f) : Filter.EventuallyConst f Filter.atTop

theorem Ordinal.eventuallyConst_of_monotone {β : Type v} [PartialOrder β] {f : Ordinal.{v} → β} [Small.{v, v} β] (hf : Monotone f) : Filter.EventuallyConst f Filter.atTop

theorem Ordinal.eventuallyConst_of_antitone {β : Type v} [PartialOrder β] {f : Ordinal.{v} → β} [Small.{v, v} β] (hf : Antitone f) : Filter.EventuallyConst f Filter.atTop