mathlib3 documentation

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 #

source
def rel_embedding.nat_lt {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : ℕ → α) (H : ∀ (n : ℕ), r (f n) (f (n + 1))) :
has_lt.lt ↪r r

If f is a strictly r-increasing sequence, then this returns f as an order embedding.

Equations
source
@[simp]
theorem rel_embedding.coe_nat_lt {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] {f : ℕ → α} {H : ∀ (n : ℕ), r (f n) (f (n + 1))} :
⇑(rel_embedding.nat_lt f H) = f
source
def rel_embedding.nat_gt {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : ℕ → α) (H : ∀ (n : ℕ), r (f (n + 1)) (f n)) :
gt ↪r r

If f is a strictly r-decreasing sequence, then this returns f as an order embedding.

Equations
source
@[simp]
theorem rel_embedding.coe_nat_gt {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] {f : ℕ → α} {H : ∀ (n : ℕ), r (f (n + 1)) (f n)} :
⇑(rel_embedding.nat_gt f H) = f
source
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
source
theorem rel_embedding.acc_iff_no_decreasing_seq {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] {x : α} :
acc r x ↔ is_empty {f // x ∈ set.range ⇑f}

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

source
theorem rel_embedding.not_acc_of_decreasing_seq {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : gt ↪r r) (k : ℕ) :
¬acc r (⇑f k)
source
theorem rel_embedding.well_founded_iff_no_descending_seq {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] :
well_founded r ↔ is_empty (gt ↪r r)

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

source
theorem rel_embedding.not_well_founded_of_decreasing_seq {α : Type u_1} {r : α → α → Prop} [is_strict_order α r] (f : gt ↪r r) :
¬well_founded r
source
def nat.order_embedding_of_set (s : set ℕ) [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] :
ℕ ↪o ℕ

An order embedding from ℕ to itself with a specified range

Equations
source
noncomputable def nat.subtype.order_iso_of_nat (s : set ℕ) [infinite ↥s] :
ℕ ≃o ↥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
source
@[simp]
theorem nat.coe_order_embedding_of_set {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] :
⇑(nat.order_embedding_of_set s) = coe ∘ nat.subtype.of_nat s
source
theorem nat.order_embedding_of_set_apply {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] {n : ℕ} :
⇑(nat.order_embedding_of_set s) n = ↑(nat.subtype.of_nat s n)
source
@[simp]
theorem nat.subtype.order_iso_of_nat_apply {s : set ℕ} [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] {n : ℕ} :
⇑(nat.subtype.order_iso_of_nat s) n = nat.subtype.of_nat s n
source
theorem nat.order_embedding_of_set_range (s : set ℕ) [infinite ↥s] [decidable_pred (λ (_x : ℕ), _x ∈ s)] :
set.range ⇑(nat.order_embedding_of_set s) = s
source
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
source
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))
source
theorem exists_increasing_or_nonincreasing_subseq {α : Type u_1} (r : α → α → Prop) [is_trans α 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 ℝ.

source
theorem well_founded.monotone_chain_condition' {α : Type u_1} [preorder α] :
well_founded gt ↔ ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬⇑a n < ⇑a m
source
theorem well_founded.monotone_chain_condition {α : Type u_1} [partial_order α] :
well_founded gt ↔ ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ⇑a n = ⇑a m

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

source
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
source
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
source
theorem well_founded.supr_eq_monotonic_sequence_limit {α : Type u_1} [complete_lattice α] (h : well_founded gt) (a : ℕ →o α) :
supr ⇑a = monotonic_sequence_limit a