# mathlib3documentation

order.order_iso_nat

# Relation embeddings from the naturals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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.coe_nat_lt {α : Type u_1} {r : α α Prop} [ r] {f : α} {H : (n : ), r (f n) (f (n + 1))} :
H) = f
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
@[simp]
theorem rel_embedding.coe_nat_gt {α : Type u_1} {r : α α Prop} [ r] {f : α} {H : (n : ), r (f (n + 1)) (f n)} :
H) = f
theorem rel_embedding.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 rel_embedding.acc_iff_no_decreasing_seq {α : Type u_1} {r : α α Prop} [ r] {x : α} :
acc r x is_empty {f // x

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

theorem rel_embedding.not_acc_of_decreasing_seq {α : Type u_1} {r : α α Prop} [ r] (f : gt ↪r r) (k : ) :
¬acc r (f k)
theorem rel_embedding.well_founded_iff_no_descending_seq {α : Type u_1} {r : α α Prop} [ r] :

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

theorem rel_embedding.not_well_founded_of_decreasing_seq {α : Type u_1} {r : α α Prop} [ r] (f : gt ↪r r) :
def nat.order_embedding_of_set (s : set ) [infinite s] [decidable_pred (λ (_x : ), _x s)] :

An order embedding from ℕ to itself with a specified range

Equations
noncomputable def nat.subtype.order_iso_of_nat (s : set ) [infinite s] :

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.

Equations
@[simp]
theorem nat.coe_order_embedding_of_set {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] :
theorem nat.order_embedding_of_set_apply {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] {n : } :
= n)
@[simp]
theorem nat.subtype.order_iso_of_nat_apply {s : set } [infinite s] [decidable_pred (λ (_x : ), _x s)] {n : } :
theorem nat.order_embedding_of_set_range (s : set ) [infinite s] [decidable_pred (λ (_x : ), _x s)] :
theorem nat.exists_subseq_of_forall_mem_union {α : Type u_1} {s t : set α} (e : α) (he : (n : ), e n s t) :
(g : ↪o ), ( (n : ), e (g n) s) (n : ), e (g n) t
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 < n r (f (g m)) (f (g n))) (m n : ), m < n ¬r (f (g m)) (f (g n))

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

theorem well_founded.monotone_chain_condition' {α : Type u_1} [preorder α] :
(a : →o α), (n : ), (m : ), n m ¬a n < a m
theorem well_founded.monotone_chain_condition {α : Type u_1}  :
(a : →o α), (n : ), (m : ), n m a n = a m

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

noncomputable def monotonic_sequence_limit_index {α : Type u_1} [preorder α] (a : →o α) :

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
noncomputable def monotonic_sequence_limit {α : Type u_1} [preorder α] (a : →o α) :
α

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

Equations