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)))
:
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 α))
:
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 α))
:
theorem
Cardinal.eventuallyConst_of_monotone
{β : Type v}
[PartialOrder β]
{f : Cardinal.{v} → β}
[Small.{v, v} β]
(hf : Monotone f)
:
theorem
Cardinal.eventuallyConst_of_antitone
{β : Type v}
[PartialOrder β]
{f : Cardinal.{v} → β}
[Small.{v, v} β]
(hf : Antitone f)
:
theorem
Ordinal.eventuallyConst_of_monotone
{β : Type v}
[PartialOrder β]
{f : Ordinal.{v} → β}
[Small.{v, v} β]
(hf : Monotone f)
:
theorem
Ordinal.eventuallyConst_of_antitone
{β : Type v}
[PartialOrder β]
{f : Ordinal.{v} → β}
[Small.{v, v} β]
(hf : Antitone f)
: