# mathlibdocumentation

order.order_iso_nat

# 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 ℕ →ₘ α.
• monotonic_sequence_limit_index: The index of the first occurence of monotonic_sequence_limit in the sequence.
def rel_embedding.nat_lt {α : Type u_1} {r : α → α → Prop} [ r] (f : → α) (H : ∀ (n : ), r (f n) (f (n + 1))) :

If f is a strictly r-increasing sequence, then this returns f as an order embedding.

Equations
@[simp]
theorem rel_embedding.nat_lt_apply {α : Type u_1} {r : α → α → Prop} [ r] {f : → α} {H : ∀ (n : ), r (f n) (f (n + 1))} {n : } :
H) n = f n
def rel_embedding.nat_gt {α : Type u_1} {r : α → α → Prop} [ r] (f : → α) (H : ∀ (n : ), r (f (n + 1)) (f n)) :

If f is a strictly r-decreasing sequence, then this returns f as an order embedding.

Equations
theorem rel_embedding.well_founded_iff_no_descending_seq {α : Type u_1} {r : α → α → Prop} [ r] :
def nat.order_embedding_of_set (s : set ) [decidable_pred (λ (_x : ), _x s)] [infinite s] :

An order embedding from ℕ to itself with a specified range

Equations

nat.subtype.of_nat as an order isomorphism between ℕ and an infinite decidable subset.

Equations
@[simp]
theorem nat.order_embedding_of_set_apply {s : set } [decidable_pred (λ (_x : ), _x s)] [infinite s] {n : } :
= n)
@[simp]
theorem nat.subtype.order_iso_of_nat_apply {s : set } [decidable_pred (λ (_x : ), _x s)] [infinite s] {n : } :
@[simp]
theorem nat.order_embedding_of_set_range (s : set ) [decidable_pred (λ (_x : ), _x s)] [infinite s] :
theorem exists_increasing_or_nonincreasing_subseq' {α : Type u_1} (r : α → α → Prop) (f : → α) :
∃ (g : ↪o ), (∀ (n : ), r (f (g n)) (f (g (n + 1)))) ∀ (m n : ), m < n¬r (f (g m)) (f (g n))
theorem exists_increasing_or_nonincreasing_subseq {α : Type u_1} (r : α → α → Prop) [ r] (f : → α) :
∃ (g : ↪o ), (∀ (m n : ), m < nr (f (g m)) (f (g n))) ∀ (m n : ), m < n¬r (f (g m)) (f (g n))
theorem well_founded.monotone_chain_condition (α : Type u_1)  :
∀ (a : →ₘ α), ∃ (n : ), ∀ (m : ), n ma n = a m

The "monotone chain condition" below is sometimes a convenient form of well foundedness.

def monotonic_sequence_limit_index {α : Type u_1} (a : →ₘ α) :

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
def monotonic_sequence_limit {α : Type u_1} (a : →ₘ α) :
α

The constant value of an eventually-constant monotone sequence a₀ ≤ a₁ ≤ a₂ ≤ ... in a partially-ordered type.

Equations
theorem well_founded.supr_eq_monotonic_sequence_limit {α : Type u_1} (h : well_founded gt) (a : →ₘ α) :
(⨆ (m : ), a m) =