doc-next-gen

Mathlib.Order.OrderIsoNat

Module docstring

{"# 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. "}
RelEmbedding.natLT definition
(f : ℕ → α) (H : ∀ n : ℕ, r (f n) (f (n + 1))) : ((· < ·) : ℕ → ℕ → Prop) ↪r r
Full source 
/-- If `f` is a strictly `r`-increasing sequence, then this returns `f` as an order embedding. -/
def natLT (f : ℕ → α) (H : ∀ n : ℕ, r (f n) (f (n + 1))) : ((· < ·) : ℕ → ℕ → Prop) ↪r r :=
  ofMonotone f <| Nat.rel_of_forall_rel_succ_of_lt r H
Order embedding from a strictly increasing sequence of natural numbers
Informal description
Given a strictly increasing sequence $f \colon \mathbb{N} \to \alpha$ with respect to a relation $r$ (i.e., $r(f(n), f(n+1))$ holds for all $n \in \mathbb{N}$), this definition returns $f$ as an order embedding from $(\mathbb{N}, <)$ to $(\alpha, r)$.
RelEmbedding.coe_natLT theorem
{f : ℕ → α} {H : ∀ n : ℕ, r (f n) (f (n + 1))} : ⇑(natLT f H) = f
Full source 
@[simp]
theorem coe_natLT {f : ℕ → α} {H : ∀ n : ℕ, r (f n) (f (n + 1))} : ⇑(natLT f H) = f :=
  rfl
Underlying Function of Order Embedding from Strictly Increasing Sequence
Informal description
For any strictly increasing sequence $f \colon \mathbb{N} \to \alpha$ with respect to a relation $r$ (i.e., $r(f(n), f(n+1))$ holds for all $n \in \mathbb{N}$), the underlying function of the order embedding $\text{natLT}(f, H)$ is equal to $f$.
RelEmbedding.natGT definition
(f : ℕ → α) (H : ∀ n : ℕ, r (f (n + 1)) (f n)) : ((· > ·) : ℕ → ℕ → Prop) ↪r r
Full source 
/-- If `f` is a strictly `r`-decreasing sequence, then this returns `f` as an order embedding. -/
def natGT (f : ℕ → α) (H : ∀ n : ℕ, r (f (n + 1)) (f n)) : ((· > ·) : ℕ → ℕ → Prop) ↪r r :=
  haveI := IsStrictOrder.swap r
  RelEmbedding.swap (natLT f H)
Order embedding from a strictly decreasing sequence of natural numbers
Informal description
Given a strictly decreasing sequence $f \colon \mathbb{N} \to \alpha$ with respect to a relation $r$ (i.e., $r(f(n+1), f(n))$ holds for all $n \in \mathbb{N}$), this definition returns $f$ as an order embedding from $(\mathbb{N}, >)$ to $(\alpha, r)$.
RelEmbedding.coe_natGT theorem
{f : ℕ → α} {H : ∀ n : ℕ, r (f (n + 1)) (f n)} : ⇑(natGT f H) = f
Full source 
@[simp]
theorem coe_natGT {f : ℕ → α} {H : ∀ n : ℕ, r (f (n + 1)) (f n)} : ⇑(natGT f H) = f :=
  rfl
Underlying Function of Order Embedding from Strictly Decreasing Sequence
Informal description
For any strictly decreasing sequence $f \colon \mathbb{N} \to \alpha$ with respect to a relation $r$ (i.e., $r(f(n+1), f(n))$ holds for all $n \in \mathbb{N}$), the underlying function of the order embedding $\mathrm{natGT}(f, H)$ is equal to $f$.
RelEmbedding.exists_not_acc_lt_of_not_acc theorem
{a : α} {r} (h : ¬Acc r a) : ∃ b, ¬Acc r b ∧ r b a
Full source 
theorem exists_not_acc_lt_of_not_acc {a : α} {r} (h : ¬Acc r a) : ∃ b, ¬Acc r b ∧ r b a := by
  contrapose! h
  refine ⟨_, fun b hr => ?_⟩
  by_contra hb
  exact h b hb hr
Existence of Non-Accessible Element Below Any Non-Accessible Element
Informal description
For any element $a$ of type $\alpha$ and a relation $r$ on $\alpha$, if $a$ is not accessible with respect to $r$ (i.e., $\neg \text{Acc } r \ a$), then there exists an element $b$ such that $b$ is also not accessible and $r \ b \ a$ holds.
RelEmbedding.acc_iff_no_decreasing_seq theorem
{x} : Acc r x ↔ IsEmpty { f : ((· > ·) : ℕ → ℕ → Prop) ↪r r // x ∈ Set.range f }
Full source 
/-- A value is accessible iff it isn't contained in any infinite decreasing sequence. -/
theorem acc_iff_no_decreasing_seq {x} :
    AccAcc r x ↔ IsEmpty { f : ((· > ·) : ℕ → ℕ → Prop) ↪r r // x ∈ Set.range f } := by
  constructor
  · refine fun h => h.recOn fun x _ IH => ?_
    constructor
    rintro ⟨f, k, hf⟩
    exact IsEmpty.elim' (IH (f (k + 1)) (hf ▸ f.map_rel_iff.2 (Nat.lt_succ_self _))) ⟨f, _, rfl⟩
  · have : ∀ x : { a // ¬Acc r a }, ∃ y : { a // ¬Acc r a }, r y.1 x.1 := by
      rintro ⟨x, hx⟩
      cases exists_not_acc_lt_of_not_acc hx with
      | intro w h => exact ⟨⟨w, h.1⟩, h.2⟩
    choose f h using this
    refine fun E =>
      by_contradiction fun hx => E.elim' ⟨natGT (fun n => (f^[n] ⟨x, hx⟩).1) fun n => ?_, 0, rfl⟩
    simp only [Function.iterate_succ']
    apply h
Accessibility Criterion via Absence of Infinite Decreasing Sequences
Informal description
An element $x$ of type $\alpha$ is accessible with respect to a relation $r$ if and only if there does not exist any order embedding $f \colon (\mathbb{N}, >) \hookrightarrow (\alpha, r)$ such that $x$ is in the range of $f$. In other words, $x$ is accessible if there is no infinite strictly decreasing sequence in $\alpha$ (with respect to $r$) that contains $x$.
RelEmbedding.not_acc_of_decreasing_seq theorem
(f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) (k : ℕ) : ¬Acc r (f k)
Full source 
theorem not_acc_of_decreasing_seq (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) (k : ℕ) : ¬Acc r (f k) := by
  rw [acc_iff_no_decreasing_seq, not_isEmpty_iff]
  exact ⟨⟨f, k, rfl⟩⟩
Inaccessibility of Elements in Infinite Decreasing Sequences
Informal description
For any order embedding $f \colon (\mathbb{N}, >) \hookrightarrow (\alpha, r)$ and any natural number $k$, the element $f(k)$ is not accessible with respect to the relation $r$.
RelEmbedding.wellFounded_iff_no_descending_seq theorem
: WellFounded r ↔ IsEmpty (((· > ·) : ℕ → ℕ → Prop) ↪r r)
Full source 
/-- 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 wellFounded_iff_no_descending_seq :
    WellFoundedWellFounded r ↔ IsEmpty (((· > ·) : ℕ → ℕ → Prop) ↪r r) := by
  constructor
  · rintro ⟨h⟩
    exact ⟨fun f => not_acc_of_decreasing_seq f 0 (h _)⟩
  · intro h
    exact ⟨fun x => acc_iff_no_decreasing_seq.2 inferInstance⟩
Well-foundedness Criterion via Absence of Infinite Decreasing Sequences
Informal description
A relation $r$ on a type $\alpha$ is well-founded if and only if there does not exist any order embedding from $(\mathbb{N}, >)$ to $(\alpha, r)$. In other words, $r$ is well-founded precisely when there are no infinite strictly decreasing sequences with respect to $r$.
RelEmbedding.not_wellFounded_of_decreasing_seq theorem
(f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) : ¬WellFounded r
Full source 
theorem not_wellFounded_of_decreasing_seq (f : ((· > ·) : ℕ → ℕ → Prop) ↪r r) : ¬WellFounded r := by
  rw [wellFounded_iff_no_descending_seq, not_isEmpty_iff]
  exact ⟨f⟩
Existence of Infinite Decreasing Sequence Implies Non-Well-Foundedness
Informal description
If there exists an order embedding $f \colon (\mathbb{N}, >) \hookrightarrow (\alpha, r)$, then the relation $r$ on $\alpha$ is not well-founded.
not_strictAnti_of_wellFoundedLT theorem
[Preorder α] [WellFoundedLT α] (f : ℕ → α) : ¬StrictAnti f
Full source 
theorem not_strictAnti_of_wellFoundedLT [Preorder α] [WellFoundedLT α] (f : ℕ → α) :
    ¬ StrictAnti f := fun hf ↦
  (RelEmbedding.natGT f (fun n ↦ hf (by simp))).not_wellFounded_of_decreasing_seq wellFounded_lt
Nonexistence of Strictly Antitone Sequences in Well-Founded Preorders
Informal description
Let $\alpha$ be a preorder with a well-founded strict less-than relation $<$. Then there does not exist a strictly antitone function $f \colon \mathbb{N} \to \alpha$ (i.e., a function such that for all $n, m \in \mathbb{N}$, $n < m$ implies $f(m) < f(n)$).
not_strictMono_of_wellFoundedGT theorem
[Preorder α] [WellFoundedGT α] (f : ℕ → α) : ¬StrictMono f
Full source 
theorem not_strictMono_of_wellFoundedGT [Preorder α] [WellFoundedGT α] (f : ℕ → α) :
    ¬ StrictMono f :=
  not_strictAnti_of_wellFoundedLT (α := αᵒᵈ) f
Nonexistence of Strictly Monotone Sequences in Well-Founded Preorders with Well-Founded GT
Informal description
Let $\alpha$ be a preorder with a well-founded strict greater-than relation $>$. Then there does not exist a strictly monotone function $f \colon \mathbb{N} \to \alpha$ (i.e., a function such that for all $n, m \in \mathbb{N}$, $n < m$ implies $f(n) < f(m)$).
Nat.orderEmbeddingOfSet definition
[DecidablePred (· ∈ s)] : ℕ ↪o ℕ
Full source 
/-- An order embedding from `ℕ` to itself with a specified range -/
def orderEmbeddingOfSet [DecidablePred (· ∈ s)] : ℕℕ ↪o ℕ :=
  (RelEmbedding.orderEmbeddingOfLTEmbedding
    (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun _ => Nat.Subtype.lt_succ_self _)).trans
    (OrderEmbedding.subtype s)
Order embedding of a decidable subset of natural numbers
Informal description
Given a decidable subset $s$ of natural numbers, this defines an order embedding from $\mathbb{N}$ to $\mathbb{N}$ that maps each natural number $n$ to the $n$-th element of $s$ (in increasing order). The embedding preserves the order structure, meaning $n \leq m$ if and only if the $n$-th element of $s$ is less than or equal to the $m$-th element of $s$.
Nat.Subtype.orderIsoOfNat definition
: ℕ ≃o s
Full source 
/-- `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. -/
noncomputable def Subtype.orderIsoOfNat : ℕℕ ≃o s := by
  classical
  exact
    RelIso.ofSurjective
      (RelEmbedding.orderEmbeddingOfLTEmbedding
        (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
      Nat.Subtype.ofNat_surjective
Order isomorphism between $\mathbb{N}$ and an infinite subset of $\mathbb{N}$
Informal description
The function `Nat.Subtype.orderIsoOfNat` constructs an order isomorphism between the natural numbers $\mathbb{N}$ and an infinite subset $s$ of $\mathbb{N}$. Specifically, it maps each natural number $n$ to the $n$-th element of $s$ in increasing order, preserving the order structure.
Nat.coe_orderEmbeddingOfSet theorem
[DecidablePred (· ∈ s)] : ⇑(orderEmbeddingOfSet s) = (↑) ∘ Subtype.ofNat s
Full source 
@[simp]
theorem coe_orderEmbeddingOfSet [DecidablePred (· ∈ s)] :
    ⇑(orderEmbeddingOfSet s) = (↑) ∘ Subtype.ofNat s :=
  rfl
Underlying Function of Order Embedding from Subset of Natural Numbers
Informal description
For any decidable subset $s$ of natural numbers, the underlying function of the order embedding `orderEmbeddingOfSet s` is equal to the composition of the canonical inclusion map from $s$ to $\mathbb{N}$ with the function `Subtype.ofNat s`, which maps each natural number $n$ to the $n$-th element of $s$.
Nat.orderEmbeddingOfSet_apply theorem
[DecidablePred (· ∈ s)] {n : ℕ} : orderEmbeddingOfSet s n = Subtype.ofNat s n
Full source 
theorem orderEmbeddingOfSet_apply [DecidablePred (· ∈ s)] {n : ℕ} :
    orderEmbeddingOfSet s n = Subtype.ofNat s n :=
  rfl
Order Embedding Maps to $n$-th Element of Subset
Informal description
For any decidable subset $s$ of natural numbers and any natural number $n$, the order embedding $\text{orderEmbeddingOfSet}(s)$ maps $n$ to the $n$-th element of $s$ (in increasing order), i.e., $\text{orderEmbeddingOfSet}(s)(n) = \text{Subtype.ofNat}(s)(n)$.
Nat.Subtype.orderIsoOfNat_apply theorem
[dP : DecidablePred (· ∈ s)] {n : ℕ} : Subtype.orderIsoOfNat s n = Subtype.ofNat s n
Full source 
@[simp]
theorem Subtype.orderIsoOfNat_apply [dP : DecidablePred (· ∈ s)] {n : ℕ} :
    Subtype.orderIsoOfNat s n = Subtype.ofNat s n := by
  simp [orderIsoOfNat]; congr!
Equality of Order Isomorphism and Subtype Construction for Natural Numbers
Informal description
For any infinite subset $s$ of natural numbers with decidable membership, the $n$-th element of $s$ under the order isomorphism $\mathbb{N} \simeq_o s$ is equal to the $n$-th element of $s$ obtained via the `Subtype.ofNat` function. In other words, for any natural number $n$, we have $\text{orderIsoOfNat}(s)(n) = \text{ofNat}(s)(n)$.
Nat.orderEmbeddingOfSet_range theorem
[DecidablePred (· ∈ s)] : Set.range (Nat.orderEmbeddingOfSet s) = s
Full source 
theorem orderEmbeddingOfSet_range [DecidablePred (· ∈ s)] :
    Set.range (Nat.orderEmbeddingOfSet s) = s :=
  Subtype.coe_comp_ofNat_range
Range of Order Embedding from Natural Numbers to Subset Equals Subset
Informal description
For any decidable subset $s$ of natural numbers, the range of the order embedding $\text{orderEmbeddingOfSet}(s) : \mathbb{N} \hookrightarrow \mathbb{N}$ is equal to $s$ itself, i.e., $\text{range}(\text{orderEmbeddingOfSet}(s)) = s$.
Nat.exists_subseq_of_forall_mem_union theorem
{s t : Set α} (e : ℕ → α) (he : ∀ n, e n ∈ s ∪ t) : ∃ g : ℕ ↪o ℕ, (∀ n, e (g n) ∈ s) ∨ ∀ n, e (g n) ∈ t
Full source 
theorem exists_subseq_of_forall_mem_union {s t : Set α} (e : ℕ → α) (he : ∀ n, e n ∈ s ∪ t) :
    ∃ g : ℕ ↪o ℕ, (∀ n, e (g n) ∈ s) ∨ ∀ n, e (g n) ∈ t := by
  classical
    have : InfiniteInfinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
      simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
    cases this
    exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
      ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
Existence of Monotone Subsequence in Union of Two Sets
Informal description
For any two sets $s$ and $t$ in a type $\alpha$, and any sequence $e : \mathbb{N} \to \alpha$ where each term $e(n)$ belongs to $s \cup t$, there exists an order embedding $g : \mathbb{N} \hookrightarrow \mathbb{N}$ such that either: 1. The subsequence $(e \circ g)(n)$ lies entirely in $s$ for all $n$, or 2. The subsequence $(e \circ g)(n)$ lies entirely in $t$ for all $n$.
exists_increasing_or_nonincreasing_subseq' theorem
(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))
Full source 
theorem exists_increasing_or_nonincreasing_subseq' (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)) := by
  classical
    let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) }
    by_cases hbad : Infinite bad
    · haveI := hbad
      refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
      have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
      rw [Nat.orderEmbeddingOfSet_range bad] at h
      exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
    · rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
      obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → ¬n ∈ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
      have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by omega, ?_⟩
        convert hn2
        omega
      let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
      exact
        ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩
Existence of Monotone or Non-Increasing Subsequence for Arbitrary Relation
Informal description
For any relation $r$ on a type $\alpha$ and any sequence $f \colon \mathbb{N} \to \alpha$, there exists an order embedding $g \colon \mathbb{N} \hookrightarrow \mathbb{N}$ such that either: 1. The subsequence $(f \circ g)$ is strictly increasing with respect to $r$, i.e., $r(f(g(n)), f(g(n+1)))$ holds for all $n \in \mathbb{N}$, or 2. The subsequence $(f \circ g)$ is non-increasing with respect to $r$, i.e., for all $m < n$ in $\mathbb{N}$, $\neg r(f(g(m)), f(g(n)))$ holds.
exists_increasing_or_nonincreasing_subseq theorem
(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))
Full source 
/-- This is the infinitary Erdős–Szekeres theorem, and an important lemma in the usual proof of
    Bolzano-Weierstrass for `ℝ`. -/
theorem exists_increasing_or_nonincreasing_subseq (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)) := by
  obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
  · refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
    obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
    induction' x with x ih
    · apply hr
    · apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))
  · exact ⟨g, Or.intro_right _ hnr⟩
Infinitary Erdős–Szekeres Theorem for Transitive Relations
Informal description
For any transitive relation $r$ on a type $\alpha$ and any sequence $f \colon \mathbb{N} \to \alpha$, there exists an order embedding $g \colon \mathbb{N} \hookrightarrow \mathbb{N}$ such that either: 1. The subsequence $(f \circ g)$ is increasing with respect to $r$, i.e., for all $m < n$ in $\mathbb{N}$, $r(f(g(m)), f(g(n)))$ holds, or 2. The subsequence $(f \circ g)$ is non-increasing with respect to $r$, i.e., for all $m < n$ in $\mathbb{N}$, $\neg r(f(g(m)), f(g(n)))$ holds.
wellFoundedGT_iff_monotone_chain_condition' theorem
[Preorder α] : WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m
Full source 
/-- 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_iff_monotone_chain_condition' [Preorder α] :
    WellFoundedGTWellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m := by
  refine ⟨fun h a => ?_, fun h => ?_⟩
  · obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)
    exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
  · rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_no_descending_seq]
    refine ⟨fun a => ?_⟩
    obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom
    exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)
Monotone chain condition for well-founded greater-than relations
Informal description
A preorder $\alpha$ is well-founded with respect to the greater-than relation $>$ if and only if for every increasing sequence $a : \mathbb{N} \to \alpha$, there exists an index $n$ such that for all $m \geq n$, the inequality $a_n < a_m$ does not hold.
WellFoundedGT.monotone_chain_condition' theorem
[Preorder α] [h : WellFoundedGT α] (a : ℕ →o α) : ∃ n, ∀ m, n ≤ m → ¬a n < a m
Full source 
theorem WellFoundedGT.monotone_chain_condition' [Preorder α] [h : WellFoundedGT α] (a : ℕℕ →o α) :
    ∃ n, ∀ m, n ≤ m → ¬a n < a m :=
  wellFoundedGT_iff_monotone_chain_condition'.1 h a
Monotone sequence stabilization in well-founded preorders
Informal description
Let $\alpha$ be a preorder with a well-founded greater-than relation $>$. For any increasing sequence $a \colon \mathbb{N} \to \alpha$, there exists an index $n$ such that for all $m \geq n$, the inequality $a_n < a_m$ does not hold.
wellFoundedGT_iff_monotone_chain_condition theorem
[PartialOrder α] : WellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m
Full source 
/-- A stronger version of the **monotone chain** condition for partial orders.

See `wellFoundedGT_iff_monotone_chain_condition'` for a version on preorders. -/
theorem wellFoundedGT_iff_monotone_chain_condition [PartialOrder α] :
    WellFoundedGTWellFoundedGT α ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m :=
  wellFoundedGT_iff_monotone_chain_condition'.trans <| by
  congrm ∀ a, ∃ n, ∀ m h, ?_
  rw [lt_iff_le_and_ne]
  simp [a.mono h]
Monotone chain condition for well-founded greater-than relations on partial orders
Informal description
For a partially ordered set $\alpha$, the greater-than relation $>$ is well-founded if and only if every increasing sequence $a \colon \mathbb{N} \to \alpha$ is eventually constant, i.e., there exists an index $n$ such that for all $m \geq n$, the equality $a_n = a_m$ holds.
WellFoundedGT.monotone_chain_condition theorem
[PartialOrder α] [h : WellFoundedGT α] (a : ℕ →o α) : ∃ n, ∀ m, n ≤ m → a n = a m
Full source 
theorem WellFoundedGT.monotone_chain_condition [PartialOrder α] [h : WellFoundedGT α] (a : ℕℕ →o α) :
    ∃ n, ∀ m, n ≤ m → a n = a m :=
  wellFoundedGT_iff_monotone_chain_condition.1 h a
Stabilization of increasing sequences in well-founded partial orders
Informal description
Let $\alpha$ be a partially ordered set with a well-founded greater-than relation $>$. For any increasing sequence $a \colon \mathbb{N} \to \alpha$, there exists an index $n$ such that for all $m \geq n$, the equality $a_n = a_m$ holds.
WellFounded.monotone_chain_condition' theorem
[Preorder α] : WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m
Full source 
@[deprecated wellFoundedGT_iff_monotone_chain_condition' (since := "2025-01-15")]
theorem WellFounded.monotone_chain_condition' [Preorder α] :
    WellFoundedWellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → ¬a n < a m := by
  rw [← isWellFounded_iff]
  exact wellFoundedGT_iff_monotone_chain_condition'
Well-foundedness of $>$ is equivalent to the monotone chain condition for preorders
Informal description
For a preorder $\alpha$, the greater-than relation $>$ is well-founded if and only if every increasing sequence $a : \mathbb{N} \to \alpha$ stabilizes in the sense that there exists an index $n$ such that for all $m \geq n$, the inequality $a_n < a_m$ does not hold.
WellFounded.monotone_chain_condition theorem
[PartialOrder α] : WellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m
Full source 
@[deprecated wellFoundedGT_iff_monotone_chain_condition (since := "2025-01-15")]
theorem WellFounded.monotone_chain_condition [PartialOrder α] :
    WellFoundedWellFounded ((· > ·) : α → α → Prop) ↔ ∀ a : ℕ →o α, ∃ n, ∀ m, n ≤ m → a n = a m := by
  rw [← isWellFounded_iff]
  exact wellFoundedGT_iff_monotone_chain_condition
Well-foundedness of $>$ is equivalent to the monotone chain condition for partial orders
Informal description
For a partially ordered set $\alpha$, the greater-than relation $>$ is well-founded if and only if every increasing sequence $a \colon \mathbb{N} \to \alpha$ is eventually constant, i.e., there exists an index $n$ such that for all $m \geq n$, the equality $a_n = a_m$ holds.
monotonicSequenceLimitIndex definition
[Preorder α] (a : ℕ →o α) : ℕ
Full source 
/-- 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 monotonicSequenceLimitIndex [Preorder α] (a : ℕℕ →o α) : ℕ :=
  sInf { n | ∀ m, n ≤ m → a n = a m }
First stabilization index of a monotone sequence
Informal description
For a monotone sequence $a_0 \leq a_1 \leq a_2 \leq \cdots$ in a preorder $\alpha$, the function `monotonicSequenceLimitIndex` returns the smallest natural number $n$ such that $a_n = a_m$ for all $m \geq n$. If the sequence is not eventually constant, the result is still defined but has no meaningful interpretation.
monotonicSequenceLimit definition
[Preorder α] (a : ℕ →o α)
Full source 
/-- The constant value of an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a
partially-ordered type. -/
noncomputable def monotonicSequenceLimit [Preorder α] (a : ℕℕ →o α) :=
  a (monotonicSequenceLimitIndex a)
Limit of an eventually-constant monotone sequence
Informal description
For a monotone sequence $a_0 \leq a_1 \leq a_2 \leq \cdots$ in a preorder $\alpha$, the function `monotonicSequenceLimit` returns the constant value that the sequence eventually stabilizes to. If the sequence is not eventually constant, the result is still defined but has no meaningful interpretation.
WellFoundedGT.iSup_eq_monotonicSequenceLimit theorem
[CompleteLattice α] [WellFoundedGT α] (a : ℕ →o α) : iSup a = monotonicSequenceLimit a
Full source 
theorem WellFoundedGT.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
    [WellFoundedGT α] (a : ℕℕ →o α) : iSup a = monotonicSequenceLimit a := by
  refine (iSup_le fun m => ?_).antisymm (le_iSup a _)
  rcases le_or_lt m (monotonicSequenceLimitIndex a) with hm | hm
  · exact a.monotone hm
  · obtain ⟨n, hn⟩ := WellFoundedGT.monotone_chain_condition' a
    have : n ∈ {n | ∀ m, n ≤ m → a n = a m} := fun k hk => (a.mono hk).eq_of_not_lt (hn k hk)
    exact (Nat.sInf_mem ⟨n, this⟩ m hm.le).ge
Supremum of Monotone Sequence Equals Its Limit in Well-Founded Lattice
Informal description
Let $\alpha$ be a complete lattice with a well-founded greater-than relation $>$. For any increasing sequence $a \colon \mathbb{N} \to \alpha$, the supremum $\bigsqcup_n a_n$ equals the limit value of the sequence, i.e., the constant value that the sequence eventually stabilizes to.
WellFounded.iSup_eq_monotonicSequenceLimit theorem
[CompleteLattice α] (h : WellFounded ((· > ·) : α → α → Prop)) (a : ℕ →o α) : iSup a = monotonicSequenceLimit a
Full source 
@[deprecated WellFoundedGT.iSup_eq_monotonicSequenceLimit (since := "2025-01-15")]
theorem WellFounded.iSup_eq_monotonicSequenceLimit [CompleteLattice α]
    (h : WellFounded ((· > ·) : α → α → Prop)) (a : ℕℕ →o α) :
    iSup a = monotonicSequenceLimit a := by
  have : WellFoundedGT α := ⟨h⟩
  exact WellFoundedGT.iSup_eq_monotonicSequenceLimit a
Supremum of Monotone Sequence Equals Its Limit in Well-Founded Lattice
Informal description
Let $\alpha$ be a complete lattice with a well-founded greater-than relation $>$. For any increasing sequence $a \colon \mathbb{N} \to \alpha$, the supremum $\bigsqcup_n a_n$ equals the limit value of the sequence, i.e., the constant value that the sequence eventually stabilizes to.
exists_covBy_seq_of_wellFoundedLT_wellFoundedGT theorem
(α) [Preorder α] [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] : ∃ a : ℕ → α, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Full source 
theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (α) [Preorder α]
    [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] :
    ∃ a : ℕ → α, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1) := by
  choose next hnext using exists_covBy_of_wellFoundedLT (α := α)
  have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›
  classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ hα trivial, ?_⟩
  have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded_of_decreasing_seq wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ fun h' ↦ wellFounded_lt.not_lt_min _ H h' h⟩
Existence of Covering Sequence in Well-Founded Preorder with Extremal Elements
Informal description
Let $\alpha$ be a nonempty preorder with well-founded strict less-than and greater-than relations. Then there exists a sequence $a \colon \mathbb{N} \to \alpha$ such that: 1. $a(0)$ is a minimal element, 2. There exists some index $n$ for which $a(n)$ is a maximal element, and 3. For all $i < n$, the element $a(i)$ is covered by $a(i+1)$ (i.e., $a(i) \lessdot a(i+1)$).
exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le theorem
{α : Type*} [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)
Full source 
theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT_of_le {α : Type*} [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) := by
  let S := Set.Icc x y
  let hS : BoundedOrder S :=
    { top := ⟨y, h, le_rfl⟩, le_top x := x.2.2, bot := ⟨x, le_rfl, h⟩, bot_le x := x.2.1 }
  obtain ⟨a, h₁, n, h₂, e⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT S
  simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂
  exact ⟨Subtype.val ∘ a, h₁, n, h₂, fun i hi ↦ ⟨(e i hi).1, fun c hc h ↦ (e i hi).2
    (c := ⟨c, (a i).2.1.trans hc.le, h.le.trans (a _).2.2⟩) hc h⟩⟩
Existence of Covering Sequence Between Elements in Well-Founded Partial Order
Informal description
Let $\alpha$ be a partially ordered set with well-founded strict less-than and greater-than relations. Given any two elements $x, y \in \alpha$ with $x \leq y$, there exists a sequence $a \colon \mathbb{N} \to \alpha$ such that: 1. $a(0) = x$, 2. There exists some index $n$ for which $a(n) = y$, and 3. For all $i < n$, the element $a(i)$ is covered by $a(i+1)$ (i.e., $a(i) \lessdot a(i+1)$).