Documentation

Mathlib.Order.OrderIsoNat

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 #

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.

Equations
Instances For
    @[simp]
    theorem RelEmbedding.coe_natLT {α : Type u_1} {r : ααProp} [IsStrictOrder α r] {f : α} {H : ∀ (n : ), r (f n) (f (n + 1))} :
    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.

    Equations
    Instances For
      @[simp]
      theorem RelEmbedding.coe_natGT {α : Type u_1} {r : ααProp} [IsStrictOrder α r] {f : α} {H : ∀ (n : ), r (f (n + 1)) (f n)} :
      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 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 (x1 x2 : ) => x1 > x2) ↪r r) :
      def Nat.orderEmbeddingOfSet (s : Set ) [Infinite s] [DecidablePred fun (x : ) => x s] :

      An order embedding from to itself with a specified range

      Equations
      Instances For
        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.

        Equations
        Instances For
          @[simp]
          theorem Nat.coe_orderEmbeddingOfSet {s : Set } [Infinite s] [DecidablePred fun (x : ) => x s] :
          @[simp]
          theorem Nat.exists_subseq_of_forall_mem_union {α : Type u_1} {s : Set α} {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 < nr (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 (x1 x2 : α) => x1 > x2) ∀ (a : →o α), ∃ (n : ), ∀ (m : ), n m¬a n < a m
          theorem WellFounded.monotone_chain_condition {α : Type u_1} [PartialOrder α] :
          (WellFounded fun (x1 x2 : α) => x1 > x2) ∀ (a : →o α), ∃ (n : ), ∀ (m : ), n ma 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.

          Equations
          Instances For
            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.

            Equations
            Instances For
              theorem WellFounded.iSup_eq_monotonicSequenceLimit {α : Type u_1} [CompleteLattice α] (h : WellFounded fun (x1 x2 : α) => x1 > x2) (a : →o α) :
              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)