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 (x1 x2 : ℕ) => x1 < x2) ↪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))} : ⇑(natLT f H) = f

def RelEmbedding.natGT {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] (f : ℕ → α) (H : ∀ (n : ℕ), r (f (n + 1)) (f n)) : (fun (x1 x2 : ℕ) => x1 > x2) ↪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)} : ⇑(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 : (fun (x1 x2 : ℕ) => x1 > x2) ↪r r // 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 (x1 x2 : ℕ) => x1 > x2) ↪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 (x1 x2 : ℕ) => x1 > x2) ↪r r)

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

See wellFounded_iff_no_descending_seq for a version which works on any relation.

theorem RelEmbedding.not_wellFounded_of_decreasing_seq {α : Type u_1} {r : α → α → Prop} [IsStrictOrder α r] (f : (fun (x1 x2 : ℕ) => x1 > x2) ↪r r) : ¬WellFounded r

theorem not_strictAnti_of_wellFoundedLT {α : Type u_1} [Preorder α] [WellFoundedLT α] (f : ℕ → α) : ¬StrictAnti f

theorem not_strictMono_of_wellFoundedGT {α : Type u_1} [Preorder α] [WellFoundedGT α] (f : ℕ → α) : ¬StrictMono f

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] : ⇑(orderEmbeddingOfSet s) = Subtype.val ∘ Subtype.ofNat s

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

@[simp]

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

theorem Nat.orderEmbeddingOfSet_range (s : Set ℕ) [Infinite ↑s] [DecidablePred fun (x : ℕ) => x ∈ s] : Set.range ⇑(orderEmbeddingOfSet s) = 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) [IsTrans α 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 wellFoundedGT_iff_monotone_chain_condition' {α : Type u_1} [Preorder α] : WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬a n < a m

The monotone chain condition: a preorder is co-well-founded iff every increasing sequence contains two non-increasing indices.

See wellFoundedGT_iff_monotone_chain_condition for a stronger version on partial orders.

theorem WellFoundedGT.monotone_chain_condition' {α : Type u_1} [Preorder α] [h : WellFoundedGT α] (a : ℕ →o α) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬a n < a m

theorem wellFoundedGT_iff_monotone_chain_condition {α : Type u_1} [PartialOrder α] : WellFoundedGT α ↔ ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → a n = a m

A stronger version of the monotone chain condition for partial orders.

See wellFoundedGT_iff_monotone_chain_condition' for a version on preorders.

theorem WellFoundedGT.monotone_chain_condition {α : Type u_1} [PartialOrder α] [h : WellFoundedGT α] (a : ℕ →o α) : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → a n = a m

@[deprecated wellFoundedGT_iff_monotone_chain_condition' (since := "2025-01-15")]

theorem WellFounded.monotone_chain_condition' {α : Type u_1} [Preorder α] : (WellFounded fun (x1 x2 : α) => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬a n < a m

@[deprecated wellFoundedGT_iff_monotone_chain_condition (since := "2025-01-15")]

theorem WellFounded.monotone_chain_condition {α : Type u_1} [PartialOrder α] : (WellFounded fun (x1 x2 : α) => x1 > x2) ↔ ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → a n = a m

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 le_monotonicSequenceLimit {α : Type u_1} [PartialOrder α] [WellFoundedGT α] (a : ℕ →o α) (m : ℕ) : a m ≤ monotonicSequenceLimit a

theorem WellFoundedGT.iSup_eq_monotonicSequenceLimit {α : Type u_1} [CompleteLattice α] [WellFoundedGT α] (a : ℕ →o α) : iSup ⇑a = monotonicSequenceLimit a

theorem WellFoundedGT.ciSup_eq_monotonicSequenceLimit {α : Type u_1} [ConditionallyCompleteLattice α] [WellFoundedGT α] (a : ℕ →o α) (ha : BddAbove (Set.range ⇑a)) : iSup ⇑a = monotonicSequenceLimit a

@[deprecated WellFoundedGT.iSup_eq_monotonicSequenceLimit (since := "2025-01-15")]

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

theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (α : Type u_2) [Preorder α] [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] : ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le {α : Type u_2} [PartialOrder α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] {x y : α} (h : x ≤ y) : ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)