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 #
An order embedding from
ℕ to itself with a specified range
nat.subtype.of_nat as an order isomorphism between
ℕ and an infinite decidable subset.
Given an eventually-constant monotone sequence
a₀ ≤ a₁ ≤ a₂ ≤ ... in a partially-ordered
monotonic_sequence_limit_index 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.