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.

ink

def RelEmbedding.natLt {α : Type u_1} {r : α → α → Prop} [inst : 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.

Equations

• RelEmbedding.natLt f H = RelEmbedding.ofMonotone f (RelEmbedding.natLt.proof_2 f H)

ink

@[simp]

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

ink

def RelEmbedding.natGt {α : Type u_1} {r : α → α → Prop} [inst : 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.

Equations

• RelEmbedding.natGt f H = RelEmbedding.swap (RelEmbedding.natLt f H)

ink

@[simp]

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

ink

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

ink

theorem RelEmbedding.acc_iff_no_decreasing_seq {α : Type u_1} {r : α → α → Prop} [inst : IsStrictOrder α r] {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.

ink

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

ink

theorem RelEmbedding.wellFounded_iff_no_descending_seq {α : Type u_1} {r : α → α → Prop} [inst : 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.

ink

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

ink

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

An order embedding from ℕ to itself with a specified range

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

theorem Nat.orderEmbeddingOfSet_range (s : Set ℕ) [inst : Infinite ↑s] [inst : DecidablePred fun x => x ∈ s] : Set.range ↑(Nat.orderEmbeddingOfSet s).toEmbedding = s

ink

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

ink

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

ink

theorem exists_increasing_or_nonincreasing_subseq {α : Type u_1} (r : α → α → Prop) [inst : IsTrans α r] (f : ℕ → α) : ∃ g, ((m n : ℕ) → m < n → r (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 ℝ.

ink

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

ink

theorem WellFounded.monotone_chain_condition {α : Type u_1} [inst : 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.

ink

noncomputable def monotonicSequenceLimitIndex {α : Type u_1} [inst : Preorder α] (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

• monotonicSequenceLimitIndex a = infₛ { n | ∀ (m : ℕ), n ≤ m → ↑a n = ↑a m }

ink

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

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

Equations

• monotonicSequenceLimit a = ↑a (monotonicSequenceLimitIndex a)

ink

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