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 α.
• monotonicSequenceLimitIndex: The index of the first occurrence of monotonicSequenceLimit in the sequence.
def RelEmbedding.natLT {α : Type u_1} {r : ααProp} [] (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
Instances For
@[simp]
theorem RelEmbedding.coe_natLT {α : Type u_1} {r : ααProp} [] {f : α} {H : ∀ (n : ), r (f n) (f (n + 1))} :
() = f
def RelEmbedding.natGT {α : Type u_1} {r : ααProp} [] (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
• = ().swap
Instances For
@[simp]
theorem RelEmbedding.coe_natGT {α : Type u_1} {r : ααProp} [] {f : α} {H : ∀ (n : ), r (f (n + 1)) (f n)} :
() = 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} [] {x : α} :
Acc r x IsEmpty { f : (fun (x x_1 : ) => x > x_1) ↪r r // x }

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} [] (f : (fun (x x_1 : ) => x > x_1) ↪r r) (k : ) :
¬Acc r (f k)
theorem RelEmbedding.wellFounded_iff_no_descending_seq {α : Type u_1} {r : ααProp} [] :
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} [] (f : (fun (x x_1 : ) => x > x_1) ↪r r) :
def Nat.orderEmbeddingOfSet (s : ) [Infinite s] [DecidablePred fun (x : ) => x s] :

An order embedding from ℕ to itself with a specified range

Equations
Instances For
noncomputable def Nat.Subtype.orderIsoOfNat (s : ) [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
Instances For
@[simp]
theorem Nat.coe_orderEmbeddingOfSet {s : } [Infinite s] [DecidablePred fun (x : ) => x s] :
= Subtype.val
theorem Nat.orderEmbeddingOfSet_apply {s : } [Infinite s] [DecidablePred fun (x : ) => x s] {n : } :
= ()
@[simp]
theorem Nat.Subtype.orderIsoOfNat_apply {s : } [Infinite s] [dP : DecidablePred fun (x : ) => x s] {n : } :
theorem Nat.orderEmbeddingOfSet_range (s : ) [Infinite s] [DecidablePred fun (x : ) => x 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 n) s) ∀ (n : ), e (g n) t
theorem exists_increasing_or_nonincreasing_subseq' {α : Type u_1} (r : ααProp) (f : α) :
∃ (g : ), (∀ (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) [IsTrans α r] (f : α) :
∃ (g : ), (∀ (m n : ), m < nr (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 WellFounded.monotone_chain_condition' {α : Type u_1} [] :
(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} [] :
(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} [] (a : →o α) :

Given an eventually-constant monotone sequence 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
Instances For
noncomputable def monotonicSequenceLimit {α : Type u_1} [] (a : →o α) :
α

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

Equations
Instances For
theorem WellFounded.iSup_eq_monotonicSequenceLimit {α : Type u_1} [] (h : WellFounded fun (x x_1 : α) => x > x_1) (a : →o α) :