Documentation

Mathlib.Order.WellFoundedSet

Well-founded sets #

A well-founded subset of an ordered type is one on which the relation < is well-founded.

Main Definitions #

Main Results #

TODO #

Prove that s is partial well ordered iff it has no infinite descending chain or antichain.

References #

Relations well-founded on sets #

def Set.WellFoundedOn {α : Type u_2} (s : Set α) (r : ααProp) :

s.WellFoundedOn r indicates that the relation r is well-founded when restricted to s.

Equations
Instances For
    @[simp]
    theorem Set.wellFoundedOn_empty {α : Type u_2} (r : ααProp) :
    theorem Set.wellFoundedOn_iff {α : Type u_2} {r : ααProp} {s : Set α} :
    Set.WellFoundedOn s r WellFounded fun a b => r a b a s b s
    @[simp]
    theorem Set.wellFoundedOn_univ {α : Type u_2} {r : ααProp} :
    theorem WellFounded.wellFoundedOn {α : Type u_2} {r : ααProp} {s : Set α} :
    @[simp]
    theorem Set.wellFoundedOn_range {α : Type u_2} {β : Type u_3} {r : ααProp} {f : βα} :
    @[simp]
    theorem Set.wellFoundedOn_image {α : Type u_2} {β : Type u_3} {r : ααProp} {f : βα} {s : Set β} :
    theorem Set.WellFoundedOn.induction {α : Type u_2} {r : ααProp} {s : Set α} {x : α} (hs : Set.WellFoundedOn s r) (hx : x s) {P : αProp} (hP : (y : α) → y s((z : α) → z sr z yP z) → P y) :
    P x
    theorem Set.WellFoundedOn.mono {α : Type u_2} {r : ααProp} {r' : ααProp} {s : Set α} {t : Set α} (h : Set.WellFoundedOn t r') (hle : r r') (hst : s t) :
    theorem Set.WellFoundedOn.mono' {α : Type u_2} {r : ααProp} {r' : ααProp} {s : Set α} (h : (a : α) → a s(b : α) → b sr' a br a b) :
    theorem Set.WellFoundedOn.subset {α : Type u_2} {r : ααProp} {s : Set α} {t : Set α} (h : Set.WellFoundedOn t r) (hst : s t) :
    theorem Set.WellFoundedOn.acc_iff_wellFoundedOn {α : Type u_6} {r : ααProp} {a : α} :

    a is accessible under the relation r iff r is well-founded on the downward transitive closure of a under r (including a or not).

    instance Set.IsStrictOrder.subset {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} :
    IsStrictOrder α fun a b => r a b a s b s
    Equations
    theorem Set.wellFoundedOn_iff_no_descending_seq {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} :
    Set.WellFoundedOn s r ∀ (f : (fun x x_1 => x > x_1) ↪r r), ¬∀ (n : ), f n s
    theorem Set.WellFoundedOn.union {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} {t : Set α} (hs : Set.WellFoundedOn s r) (ht : Set.WellFoundedOn t r) :
    @[simp]
    theorem Set.wellFoundedOn_union {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} {t : Set α} :

    Sets well-founded w.r.t. the strict inequality #

    def Set.IsWf {α : Type u_2} [LT α] (s : Set α) :

    s.IsWf indicates that < is well-founded when restricted to s.

    Equations
    Instances For
      @[simp]
      theorem Set.isWf_empty {α : Type u_2} [LT α] :
      theorem Set.isWf_univ_iff {α : Type u_2} [LT α] :
      Set.IsWf Set.univ WellFounded fun x x_1 => x < x_1
      theorem Set.IsWf.mono {α : Type u_2} [LT α] {s : Set α} {t : Set α} (h : Set.IsWf t) (st : s t) :
      theorem Set.IsWf.union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} (hs : Set.IsWf s) (ht : Set.IsWf t) :
      @[simp]
      theorem Set.isWf_union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} :
      theorem Set.isWf_iff_no_descending_seq {α : Type u_2} [Preorder α] {s : Set α} :
      Set.IsWf s ∀ (f : α), StrictAnti f¬∀ (n : ), f (OrderDual.toDual n) s

      Partially well-ordered sets #

      A set is partially well-ordered by a relation r when any infinite sequence contains two elements where the first is related to the second by r. Equivalently, any antichain (see IsAntichain) is finite, see Set.partiallyWellOrderedOn_iff_finite_antichains.

      def Set.PartiallyWellOrderedOn {α : Type u_2} (s : Set α) (r : ααProp) :

      A subset is partially well-ordered by a relation r when any infinite sequence contains two elements where the first is related to the second by r.

      Equations
      Instances For
        theorem Set.PartiallyWellOrderedOn.mono {α : Type u_2} {r : ααProp} {s : Set α} {t : Set α} (ht : Set.PartiallyWellOrderedOn t r) (h : s t) :
        @[simp]
        theorem Set.partiallyWellOrderedOn_empty {α : Type u_2} (r : ααProp) :
        theorem Set.PartiallyWellOrderedOn.union {α : Type u_2} {r : ααProp} {s : Set α} {t : Set α} (hs : Set.PartiallyWellOrderedOn s r) (ht : Set.PartiallyWellOrderedOn t r) :
        theorem Set.PartiallyWellOrderedOn.image_of_monotone_on {α : Type u_2} {β : Type u_3} {r : ααProp} {r' : ββProp} {f : αβ} {s : Set α} (hs : Set.PartiallyWellOrderedOn s r) (hf : (a₁ : α) → a₁ s(a₂ : α) → a₂ sr a₁ a₂r' (f a₁) (f a₂)) :
        theorem IsAntichain.finite_of_partiallyWellOrderedOn {α : Type u_2} {r : ααProp} {s : Set α} (ha : IsAntichain r s) (hp : Set.PartiallyWellOrderedOn s r) :
        theorem Set.Finite.partiallyWellOrderedOn {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (hs : Set.Finite s) :
        theorem IsAntichain.partiallyWellOrderedOn_iff {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (hs : IsAntichain r s) :
        @[simp]
        theorem Set.partiallyWellOrderedOn_singleton {α : Type u_2} {r : ααProp} [IsRefl α r] (a : α) :
        theorem Set.Subsingleton.partiallyWellOrderedOn {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (hs : Set.Subsingleton s) :
        @[simp]
        theorem Set.partiallyWellOrderedOn_insert {α : Type u_2} {r : ααProp} {s : Set α} {a : α} [IsRefl α r] :
        theorem Set.PartiallyWellOrderedOn.insert {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (h : Set.PartiallyWellOrderedOn s r) (a : α) :
        theorem Set.partiallyWellOrderedOn_iff_finite_antichains {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] [IsSymm α r] :
        Set.PartiallyWellOrderedOn s r ∀ (t : Set α), t sIsAntichain r tSet.Finite t
        theorem Set.PartiallyWellOrderedOn.exists_monotone_subseq {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] [IsTrans α r] (h : Set.PartiallyWellOrderedOn s r) (f : α) (hf : ∀ (n : ), f n s) :
        g, (m n : ) → m nr (f (g m)) (f (g n))
        theorem Set.partiallyWellOrderedOn_iff_exists_monotone_subseq {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] [IsTrans α r] :
        Set.PartiallyWellOrderedOn s r ∀ (f : α), (∀ (n : ), f n s) → g, (m n : ) → m nr (f (g m)) (f (g n))
        theorem Set.PartiallyWellOrderedOn.prod {α : Type u_2} {β : Type u_3} {r : ααProp} {r' : ββProp} {s : Set α} [IsRefl α r] [IsTrans α r] {t : Set β} (hs : Set.PartiallyWellOrderedOn s r) (ht : Set.PartiallyWellOrderedOn t r') :
        Set.PartiallyWellOrderedOn (s ×ˢ t) fun x y => r x.fst y.fst r' x.snd y.snd
        theorem Set.PartiallyWellOrderedOn.wellFoundedOn {α : Type u_2} {r : ααProp} {s : Set α} [IsPreorder α r] (h : Set.PartiallyWellOrderedOn s r) :
        Set.WellFoundedOn s fun a b => r a b ¬r b a
        def Set.IsPwo {α : Type u_2} [Preorder α] (s : Set α) :

        A subset of a preorder is partially well-ordered when any infinite sequence contains a monotone subsequence of length 2 (or equivalently, an infinite monotone subsequence).

        Equations
        Instances For
          theorem Set.IsPwo.mono {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} (ht : Set.IsPwo t) :
          s tSet.IsPwo s
          theorem Set.IsPwo.exists_monotone_subseq {α : Type u_2} [Preorder α] {s : Set α} (h : Set.IsPwo s) (f : α) (hf : ∀ (n : ), f n s) :
          g, Monotone (f g)
          theorem Set.isPwo_iff_exists_monotone_subseq {α : Type u_2} [Preorder α] {s : Set α} :
          Set.IsPwo s ∀ (f : α), (∀ (n : ), f n s) → g, Monotone (f g)
          theorem Set.IsPwo.isWf {α : Type u_2} [Preorder α] {s : Set α} (h : Set.IsPwo s) :
          theorem Set.IsPwo.prod {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : Set.IsPwo s) (ht : Set.IsPwo t) :
          theorem Set.IsPwo.image_of_monotoneOn {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} (hs : Set.IsPwo s) {f : αβ} (hf : MonotoneOn f s) :
          theorem Set.IsPwo.image_of_monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} (hs : Set.IsPwo s) {f : αβ} (hf : Monotone f) :
          theorem Set.IsPwo.union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} (hs : Set.IsPwo s) (ht : Set.IsPwo t) :
          @[simp]
          theorem Set.isPwo_union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} :
          theorem Set.Finite.isPwo {α : Type u_2} [Preorder α] {s : Set α} (hs : Set.Finite s) :
          @[simp]
          theorem Set.isPwo_of_finite {α : Type u_2} [Preorder α] {s : Set α} [Finite α] :
          @[simp]
          theorem Set.isPwo_singleton {α : Type u_2} [Preorder α] (a : α) :
          @[simp]
          theorem Set.isPwo_empty {α : Type u_2} [Preorder α] :
          theorem Set.Subsingleton.isPwo {α : Type u_2} [Preorder α] {s : Set α} (hs : Set.Subsingleton s) :
          @[simp]
          theorem Set.isPwo_insert {α : Type u_2} [Preorder α] {s : Set α} {a : α} :
          theorem Set.IsPwo.insert {α : Type u_2} [Preorder α] {s : Set α} (h : Set.IsPwo s) (a : α) :
          theorem Set.Finite.isWf {α : Type u_2} [Preorder α] {s : Set α} (hs : Set.Finite s) :
          @[simp]
          theorem Set.isWf_singleton {α : Type u_2} [Preorder α] {a : α} :
          theorem Set.Subsingleton.isWf {α : Type u_2} [Preorder α] {s : Set α} (hs : Set.Subsingleton s) :
          @[simp]
          theorem Set.isWf_insert {α : Type u_2} [Preorder α] {s : Set α} {a : α} :
          theorem Set.IsWf.insert {α : Type u_2} [Preorder α] {s : Set α} (h : Set.IsWf s) (a : α) :
          theorem Set.Finite.wellFoundedOn {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} (hs : Set.Finite s) :
          @[simp]
          theorem Set.wellFoundedOn_singleton {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {a : α} :
          theorem Set.Subsingleton.wellFoundedOn {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} (hs : Set.Subsingleton s) :
          @[simp]
          theorem Set.wellFoundedOn_insert {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} {a : α} :
          theorem Set.WellFoundedOn.insert {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} (h : Set.WellFoundedOn s r) (a : α) :
          theorem Set.IsWf.isPwo {α : Type u_2} [LinearOrder α] {s : Set α} (hs : Set.IsWf s) :
          theorem Set.isWf_iff_isPwo {α : Type u_2} [LinearOrder α] {s : Set α} :

          In a linear order, the predicates Set.IsWf and Set.IsPwo are equivalent.

          @[simp]
          theorem Finset.partiallyWellOrderedOn {α : Type u_2} {r : ααProp} [IsRefl α r] (s : Finset α) :
          @[simp]
          theorem Finset.isPwo {α : Type u_2} [Preorder α] (s : Finset α) :
          @[simp]
          theorem Finset.isWf {α : Type u_2} [Preorder α] (s : Finset α) :
          @[simp]
          theorem Finset.wellFoundedOn {α : Type u_2} {r : ααProp} [IsStrictOrder α r] (s : Finset α) :
          theorem Finset.wellFoundedOn_sup {ι : Type u_1} {α : Type u_2} {r : ααProp} [IsStrictOrder α r] (s : Finset ι) {f : ιSet α} :
          Set.WellFoundedOn (Finset.sup s f) r ∀ (i : ι), i sSet.WellFoundedOn (f i) r
          theorem Finset.partiallyWellOrderedOn_sup {ι : Type u_1} {α : Type u_2} {r : ααProp} (s : Finset ι) {f : ιSet α} :
          theorem Finset.isWf_sup {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          Set.IsWf (Finset.sup s f) ∀ (i : ι), i sSet.IsWf (f i)
          theorem Finset.isPwo_sup {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          Set.IsPwo (Finset.sup s f) ∀ (i : ι), i sSet.IsPwo (f i)
          @[simp]
          theorem Finset.wellFoundedOn_bUnion {ι : Type u_1} {α : Type u_2} {r : ααProp} [IsStrictOrder α r] (s : Finset ι) {f : ιSet α} :
          Set.WellFoundedOn (⋃ (i : ι) (_ : i s), f i) r ∀ (i : ι), i sSet.WellFoundedOn (f i) r
          @[simp]
          theorem Finset.partiallyWellOrderedOn_bUnion {ι : Type u_1} {α : Type u_2} {r : ααProp} (s : Finset ι) {f : ιSet α} :
          Set.PartiallyWellOrderedOn (⋃ (i : ι) (_ : i s), f i) r ∀ (i : ι), i sSet.PartiallyWellOrderedOn (f i) r
          @[simp]
          theorem Finset.isWf_bUnion {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          Set.IsWf (⋃ (i : ι) (_ : i s), f i) ∀ (i : ι), i sSet.IsWf (f i)
          @[simp]
          theorem Finset.isPwo_bUnion {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          Set.IsPwo (⋃ (i : ι) (_ : i s), f i) ∀ (i : ι), i sSet.IsPwo (f i)
          noncomputable def Set.IsWf.min {α : Type u_2} [Preorder α] {s : Set α} (hs : Set.IsWf s) (hn : Set.Nonempty s) :
          α

          Set.IsWf.min returns a minimal element of a nonempty well-founded set.

          Equations
          Instances For
            theorem Set.IsWf.min_mem {α : Type u_2} [Preorder α] {s : Set α} (hs : Set.IsWf s) (hn : Set.Nonempty s) :
            theorem Set.IsWf.not_lt_min {α : Type u_2} [Preorder α] {s : Set α} {a : α} (hs : Set.IsWf s) (hn : Set.Nonempty s) (ha : a s) :
            @[simp]
            theorem Set.isWf_min_singleton {α : Type u_2} [Preorder α] (a : α) {hs : Set.IsWf {a}} {hn : Set.Nonempty {a}} :
            Set.IsWf.min hs hn = a
            theorem Set.IsWf.min_le {α : Type u_2} [LinearOrder α] {s : Set α} {a : α} (hs : Set.IsWf s) (hn : Set.Nonempty s) (ha : a s) :
            theorem Set.IsWf.le_min_iff {α : Type u_2} [LinearOrder α] {s : Set α} {a : α} (hs : Set.IsWf s) (hn : Set.Nonempty s) :
            a Set.IsWf.min hs hn ∀ (b : α), b sa b
            theorem Set.IsWf.min_le_min_of_subset {α : Type u_2} [LinearOrder α] {s : Set α} {t : Set α} {hs : Set.IsWf s} {hsn : Set.Nonempty s} {ht : Set.IsWf t} {htn : Set.Nonempty t} (hst : s t) :
            theorem Set.IsWf.min_union {α : Type u_2} [LinearOrder α] {s : Set α} {t : Set α} (hs : Set.IsWf s) (hsn : Set.Nonempty s) (ht : Set.IsWf t) (htn : Set.Nonempty t) :
            Set.IsWf.min (_ : Set.IsWf (s t)) (_ : Set.Nonempty (s t)) = min (Set.IsWf.min hs hsn) (Set.IsWf.min ht htn)
            def Set.PartiallyWellOrderedOn.IsBadSeq {α : Type u_2} (r : ααProp) (s : Set α) (f : α) :

            In the context of partial well-orderings, a bad sequence is a nonincreasing sequence whose range is contained in a particular set s. One exists if and only if s is not partially well-ordered.

            Equations
            Instances For
              def Set.PartiallyWellOrderedOn.IsMinBadSeq {α : Type u_2} (r : ααProp) (rk : α) (s : Set α) (n : ) (f : α) :

              This indicates that every bad sequence g that agrees with f on the first n terms has rk (f n) ≤ rk (g n).

              Equations
              Instances For
                noncomputable def Set.PartiallyWellOrderedOn.minBadSeqOfBadSeq {α : Type u_2} (r : ααProp) (rk : α) (s : Set α) (n : ) (f : α) (hf : Set.PartiallyWellOrderedOn.IsBadSeq r s f) :
                { g // (∀ (m : ), m < nf m = g m) Set.PartiallyWellOrderedOn.IsBadSeq r s g Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n g }

                Given a bad sequence f, this constructs a bad sequence that agrees with f on the first n terms and is minimal at n.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  theorem Set.PartiallyWellOrderedOn.exists_min_bad_of_exists_bad {α : Type u_2} (r : ααProp) (rk : α) (s : Set α) :
                  theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ {α : Type u_2} (r : ααProp) [IsRefl α r] [IsTrans α r] {s : Set α} (h : Set.PartiallyWellOrderedOn s r) :
                  Set.PartiallyWellOrderedOn {l | ∀ (x : α), x lx s} (List.SublistForall₂ r)

                  Higman's Lemma, which states that for any reflexive, transitive relation r which is partially well-ordered on a set s, the relation List.SublistForall₂ r is partially well-ordered on the set of lists of elements of s. That relation is defined so that List.SublistForall₂ r l₁ l₂ whenever l₁ related pointwise by r to a sublist of l₂.

                  theorem WellFounded.isWf {α : Type u_2} [LT α] (h : WellFounded fun x x_1 => x < x_1) (s : Set α) :
                  theorem Pi.isPwo {ι : Type u_1} {α : ιType u_6} [(i : ι) → LinearOrder (α i)] [∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1] [Finite ι] (s : Set ((i : ι) → α i)) :

                  A version of Dickson's lemma any subset of functions Π s : σ, α s is partially well ordered, when σ is a Fintype and each α s is a linear well order. This includes the classical case of Dickson's lemma that ℕ ^ n is a well partial order. Some generalizations would be possible based on this proof, to include cases where the target is partially well ordered, and also to consider the case of Set.PartiallyWellOrderedOn instead of Set.IsPwo.

                  theorem WellFounded.prod_lex_of_wellFoundedOn_fiber {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : ααProp} {rβ : ββProp} {f : γα} {g : γβ} (hα : WellFounded ( on f)) (hβ : ∀ (a : α), Set.WellFoundedOn (f ⁻¹' {a}) ( on g)) :
                  WellFounded (Prod.Lex on fun c => (f c, g c))

                  Stronger version of WellFounded.prod_lex. Instead of requiring rβ on g to be well-founded, we only require it to be well-founded on fibers of f.

                  theorem Set.WellFoundedOn.prod_lex_of_wellFoundedOn_fiber {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : ααProp} {rβ : ββProp} {f : γα} {g : γβ} {s : Set γ} (hα : Set.WellFoundedOn s ( on f)) (hβ : ∀ (a : α), Set.WellFoundedOn (s f ⁻¹' {a}) ( on g)) :
                  Set.WellFoundedOn s (Prod.Lex on fun c => (f c, g c))
                  theorem WellFounded.sigma_lex_of_wellFoundedOn_fiber {ι : Type u_1} {γ : Type u_4} {π : ιType u_5} {rι : ιιProp} {rπ : (i : ι) → π iπ iProp} {f : γι} {g : (i : ι) → γπ i} (hι : WellFounded ( on f)) (hπ : ∀ (i : ι), Set.WellFoundedOn (f ⁻¹' {i}) ( i on g i)) :
                  WellFounded (Sigma.Lex on fun c => { fst := f c, snd := g (f c) c })

                  Stronger version of PSigma.lex_wf. Instead of requiring rπ on g to be well-founded, we only require it to be well-founded on fibers of f.

                  theorem Set.WellFoundedOn.sigma_lex_of_wellFoundedOn_fiber {ι : Type u_1} {γ : Type u_4} {π : ιType u_5} {rι : ιιProp} {rπ : (i : ι) → π iπ iProp} {f : γι} {g : (i : ι) → γπ i} {s : Set γ} (hι : Set.WellFoundedOn s ( on f)) (hπ : ∀ (i : ι), Set.WellFoundedOn (s f ⁻¹' {i}) ( i on g i)) :
                  Set.WellFoundedOn s (Sigma.Lex on fun c => { fst := f c, snd := g (f c) c })