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} [IsStrictOrder α r] (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.

@[simp]

theorem RelEmbedding.coe_natLT {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] {f : ℕ → α} {H : (n : ℕ) → r (f n) (f (n + 1))} : ↑(RelEmbedding.natLT f H) = f

def RelEmbedding.natGT {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] (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.

@[simp]

theorem RelEmbedding.coe_natGT {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] {f : ℕ → α} {H : (n : ℕ) → r (f (n + 1)) (f n)} : ↑(RelEmbedding.natGT f H) = 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} [IsStrictOrder α r] {x : α} : Acc r x ↔ IsEmpty { f // x ∈ Set.range ↑f }

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} [IsStrictOrder α r] (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} [IsStrictOrder α r] : WellFounded r ↔ 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} [IsStrictOrder α r] (f : (fun x x_1 => x > x_1) ↪r r) : ¬WellFounded r

def Nat.orderEmbeddingOfSet (s : Set ℕ) [Infinite ↑s] [DecidablePred fun x => x ∈ s] : ℕ ↪o ℕ

An order embedding from ℕ to itself with a specified range

noncomputable def Nat.Subtype.orderIsoOfNat (s : Set ℕ) [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.

@[simp]

theorem Nat.coe_orderEmbeddingOfSet {s : Set ℕ} [Infinite ↑s] [DecidablePred fun x => x ∈ s] : ↑(Nat.orderEmbeddingOfSet s) = Subtype.val ∘ Nat.Subtype.ofNat s

theorem Nat.orderEmbeddingOfSet_apply {s : Set ℕ} [Infinite ↑s] [DecidablePred fun x => x ∈ s] {n : ℕ} : ↑(Nat.orderEmbeddingOfSet s) n = ↑(Nat.Subtype.ofNat s n)

@[simp]

theorem Nat.Subtype.orderIsoOfNat_apply {s : Set ℕ} [Infinite ↑s] [dP : DecidablePred fun x => x ∈ s] {n : ℕ} : ↑(Nat.Subtype.orderIsoOfNat s) n = Nat.Subtype.ofNat s n

theorem Nat.orderEmbeddingOfSet_range (s : Set ℕ) [Infinite ↑s] [DecidablePred fun x => x ∈ s] : Set.range ↑(Nat.orderEmbeddingOfSet s) = 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 < 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 WellFounded.monotone_chain_condition' {α : Type u_1} [Preorder α] : (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} [PartialOrder α] : (WellFounded fun x x_1 => x > x_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 monotonicSequenceLimitIndex {α : Type u_1} [Preorder α] (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.

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

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

theorem WellFounded.iSup_eq_monotonicSequenceLimit {α : Type u_1} [CompleteLattice α] (h : WellFounded fun x x_1 => x > x_1) (a : ℕ →o α) : iSup ↑a = monotonicSequenceLimit a