Relation embeddings from the naturals #
This file allows translation from monotone functions
ℕ → α to order embeddings
ℕ ↪ α and
defines the limit value of an eventually-constant sequence.
Main declarations #
This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of
Given an eventually-constant monotone sequence
a₀ ≤ a₁ ≤ a₂ ≤ ... in a partially-ordered
monotonicSequenceLimitIndex a is the least natural number
n for which
aₙ reaches the
constant value. For sequences that are not eventually constant,
is defined, but is a junk value.