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 #
nat_lt
/nat_gt
: Make an order embeddingℕ ↪ α
from an increasing/decreasing functionℕ → α
.monotonic_sequence_limit
: The limit of an eventually-constant monotone sequenceℕ →o α
.monotonic_sequence_limit_index
: The index of the first occurence ofmonotonic_sequence_limit
in the sequence.
If f
is a strictly r
-increasing sequence, then this returns f
as an order embedding.
Equations
If f
is a strictly r
-decreasing sequence, then this returns f
as an order embedding.
Equations
- rel_embedding.nat_gt f H = (rel_embedding.nat_lt f H).swap
An order embedding from ℕ
to itself with a specified range
nat.subtype.of_nat
as an order isomorphism between ℕ
and an infinite subset. See also
nat.nth
for a version where the subset may be finite.
This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of
Bolzano-Weierstrass for ℝ
.
The "monotone chain condition" below is sometimes a convenient form of well foundedness.
Given an eventually-constant monotone sequence a₀ ≤ a₁ ≤ a₂ ≤ ...
in a partially-ordered
type, 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, monotonic_sequence_limit_index a
is defined, but is a junk value.
Equations
- monotonic_sequence_limit_index a = has_Inf.Inf {n : ℕ | ∀ (m : ℕ), n ≤ m → ⇑a n = ⇑a m}
The constant value of an eventually-constant monotone sequence a₀ ≤ a₁ ≤ a₂ ≤ ...
in a
partially-ordered type.