# Documentation

Mathlib.Order.OrderIsoNat

# 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 #

• natLt/natGt: Make an order embedding Nat ↪ α↪ α from an increasing/decreasing function Nat → α→ α.
• monotonicSequenceLimit: The limit of an eventually-constant monotone sequence Nat →o α→o α.
• monotonicSequenceLimitIndex: The index of the first occurence of monotonicSequenceLimit in the sequence.
def RelEmbedding.natLt {α : Type u_1} {r : ααProp} [inst : ] (f : α) (H : (n : ) → r (f n) (f (n + 1))) :
(fun x x_1 => x < x_1) ↪r r

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

Equations
@[simp]
theorem RelEmbedding.coe_natLt {α : Type u_1} {r : ααProp} [inst : ] {f : α} {H : (n : ) → r (f n) (f (n + 1))} :
().toEmbedding = f
def RelEmbedding.natGt {α : Type u_1} {r : ααProp} [inst : ] (f : α) (H : (n : ) → r (f (n + 1)) (f n)) :
(fun x x_1 => x > x_1) ↪r r

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

Equations
@[simp]
theorem RelEmbedding.coe_natGt {α : Type u_1} {r : ααProp} [inst : ] {f : α} {H : (n : ) → r (f (n + 1)) (f n)} :
().toEmbedding = f
theorem RelEmbedding.exists_not_acc_lt_of_not_acc {α : Type u_1} {a : α} {r : ααProp} (h : ¬Acc r a) :
b, ¬Acc r b r b a
theorem RelEmbedding.acc_iff_no_decreasing_seq {α : Type u_1} {r : ααProp} [inst : ] {x : α} :
Acc r x IsEmpty { f // x Set.range f.toEmbedding }

A value is accessible iff it isn't contained in any infinite decreasing sequence.

theorem RelEmbedding.not_acc_of_decreasing_seq {α : Type u_1} {r : ααProp} [inst : ] (f : (fun x x_1 => x > x_1) ↪r r) (k : ) :
¬Acc r (f.toEmbedding k)
theorem RelEmbedding.wellFounded_iff_no_descending_seq {α : Type u_1} {r : ααProp} [inst : ] :
IsEmpty ((fun x x_1 => x > x_1) ↪r r)

A relation is well-founded iff it doesn't have any infinite decreasing sequence.

theorem RelEmbedding.not_wellFounded_of_decreasing_seq {α : Type u_1} {r : ααProp} [inst : ] (f : (fun x x_1 => x > x_1) ↪r r) :
def Nat.orderEmbeddingOfSet (s : ) [inst : Infinite s] [inst : DecidablePred fun x => x s] :

An order embedding from ℕ to itself with a specified range

Equations
• One or more equations did not get rendered due to their size.
noncomputable def Nat.Subtype.orderIsoOfNat (s : ) [inst : Infinite s] :
≃o s

Nat.Subtype.ofNat as an order isomorphism between ℕ and an infinite subset. See also Nat.Nth for a version where the subset may be finite.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Nat.coe_orderEmbeddingOfSet {s : } [inst : Infinite s] [inst : DecidablePred fun x => x s] :
().toEmbedding = Subtype.val
theorem Nat.orderEmbeddingOfSet_apply {s : } [inst : Infinite s] [inst : DecidablePred fun x => x s] {n : } :
().toEmbedding n = ↑()
@[simp]
theorem Nat.Subtype.orderIsoOfNat_apply {s : } [inst : Infinite s] [dP : DecidablePred fun x => x s] {n : } :
().toEmbedding n =
theorem Nat.orderEmbeddingOfSet_range (s : ) [inst : Infinite s] [inst : DecidablePred fun x => x s] :
Set.range ().toEmbedding = s
theorem Nat.exists_subseq_of_forall_mem_union {α : Type u_1} {s : Set α} {t : Set α} (e : α) (he : ∀ (n : ), e n s t) :
g, (∀ (n : ), e (g.toEmbedding n) s) ∀ (n : ), e (g.toEmbedding n) t
theorem exists_increasing_or_nonincreasing_subseq' {α : Type u_1} (r : ααProp) (f : α) :
g, ((n : ) → r (f (g.toEmbedding n)) (f (g.toEmbedding (n + 1)))) ∀ (m n : ), m < n¬r (f (g.toEmbedding m)) (f (g.toEmbedding n))
theorem exists_increasing_or_nonincreasing_subseq {α : Type u_1} (r : ααProp) [inst : IsTrans α r] (f : α) :
g, ((m n : ) → m < nr (f (g.toEmbedding m)) (f (g.toEmbedding n))) ∀ (m n : ), m < n¬r (f (g.toEmbedding m)) (f (g.toEmbedding n))

This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of Bolzano-Weierstrass for ℝ.

theorem WellFounded.monotone_chain_condition' {α : Type u_1} [inst : ] :
(WellFounded fun x x_1 => x > x_1) ∀ (a : →o α), n, ∀ (m : ), n m¬a n < a m
theorem WellFounded.monotone_chain_condition {α : Type u_1} [inst : ] :
(WellFounded fun x x_1 => x > x_1) ∀ (a : →o α), n, ∀ (m : ), n ma n = a m

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

noncomputable def monotonicSequenceLimitIndex {α : Type u_1} [inst : ] (a : →o α) :

Given an eventually-constant monotone sequence a₀ ≤ a₁ ≤ a₂ ≤ ...≤ a₁ ≤ a₂ ≤ ...≤ a₂ ≤ ...≤ ... in a partially-ordered type, monotonicSequenceLimitIndex a is the least natural number n for which aₙ reaches the constant value. For sequences that are not eventually constant, monotonicSequenceLimitIndex a is defined, but is a junk value.

Equations
noncomputable def monotonicSequenceLimit {α : Type u_1} [inst : ] (a : →o α) :
α

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

Equations
theorem WellFounded.supᵢ_eq_monotonicSequenceLimit {α : Type u_1} [inst : ] (h : WellFounded fun x x_1 => x > x_1) (a : →o α) :