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
  • s.WellFoundedOn r = WellFounded fun (a b : s) => r a b
Instances For
    @[simp]
    theorem Set.wellFoundedOn_empty {α : Type u_2} (r : ααProp) :
    .WellFoundedOn r
    theorem Set.wellFoundedOn_iff {α : Type u_2} {r : ααProp} {s : Set α} :
    s.WellFoundedOn r WellFounded fun (a b : α) => r a b a s b s
    @[simp]
    theorem Set.wellFoundedOn_univ {α : Type u_2} {r : ααProp} :
    Set.univ.WellFoundedOn r WellFounded r
    theorem WellFounded.wellFoundedOn {α : Type u_2} {r : ααProp} {s : Set α} :
    WellFounded rs.WellFoundedOn r
    @[simp]
    theorem Set.wellFoundedOn_range {α : Type u_2} {β : Type u_3} {r : ααProp} {f : βα} :
    (Set.range f).WellFoundedOn r WellFounded (r on f)
    @[simp]
    theorem Set.wellFoundedOn_image {α : Type u_2} {β : Type u_3} {r : ααProp} {f : βα} {s : Set β} :
    (f '' s).WellFoundedOn r s.WellFoundedOn (r on f)
    theorem Set.WellFoundedOn.induction {α : Type u_2} {r : ααProp} {s : Set α} {x : α} (hs : s.WellFoundedOn r) (hx : x s) {P : αProp} (hP : ys, (∀ zs, r z yP z)P y) :
    P x
    theorem Set.WellFoundedOn.mono {α : Type u_2} {r : ααProp} {r' : ααProp} {s : Set α} {t : Set α} (h : t.WellFoundedOn r') (hle : r r') (hst : s t) :
    s.WellFoundedOn r
    theorem Set.WellFoundedOn.mono' {α : Type u_2} {r : ααProp} {r' : ααProp} {s : Set α} (h : as, bs, r' a br a b) :
    s.WellFoundedOn rs.WellFoundedOn r'
    theorem Set.WellFoundedOn.subset {α : Type u_2} {r : ααProp} {s : Set α} {t : Set α} (h : t.WellFoundedOn r) (hst : s t) :
    s.WellFoundedOn r
    theorem Set.WellFoundedOn.acc_iff_wellFoundedOn {α : Type u_6} {r : ααProp} {a : α} :
    [Acc r a, {b : α | Relation.ReflTransGen r b a}.WellFoundedOn r, {b : α | Relation.TransGen r b a}.WellFoundedOn r].TFAE

    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 α} :
    s.WellFoundedOn r ∀ (f : (fun (x1 x2 : ) => x1 > x2) ↪r r), ¬∀ (n : ), f n s
    theorem Set.WellFoundedOn.union {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} {t : Set α} (hs : s.WellFoundedOn r) (ht : t.WellFoundedOn r) :
    (s t).WellFoundedOn r
    @[simp]
    theorem Set.wellFoundedOn_union {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} {t : Set α} :
    (s t).WellFoundedOn r s.WellFoundedOn r t.WellFoundedOn r

    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
    • s.IsWF = s.WellFoundedOn fun (x1 x2 : α) => x1 < x2
    Instances For
      @[simp]
      theorem Set.isWF_empty {α : Type u_2} [LT α] :
      .IsWF
      theorem Set.isWF_univ_iff {α : Type u_2} [LT α] :
      Set.univ.IsWF WellFounded fun (x1 x2 : α) => x1 < x2
      theorem Set.IsWF.mono {α : Type u_2} [LT α] {s : Set α} {t : Set α} (h : t.IsWF) (st : s t) :
      s.IsWF
      theorem Set.IsWF.union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) :
      (s t).IsWF
      @[simp]
      theorem Set.isWF_union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} :
      (s t).IsWF s.IsWF t.IsWF
      theorem Set.isWF_iff_no_descending_seq {α : Type u_2} [Preorder α] {s : Set α} :
      s.IsWF ∀ (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
      • s.PartiallyWellOrderedOn r = ∀ (f : α), (∀ (n : ), f n s)∃ (m : ) (n : ), m < n r (f m) (f n)
      Instances For
        theorem Set.PartiallyWellOrderedOn.mono {α : Type u_2} {r : ααProp} {s : Set α} {t : Set α} (ht : t.PartiallyWellOrderedOn r) (h : s t) :
        s.PartiallyWellOrderedOn r
        @[simp]
        theorem Set.partiallyWellOrderedOn_empty {α : Type u_2} (r : ααProp) :
        .PartiallyWellOrderedOn r
        theorem Set.PartiallyWellOrderedOn.union {α : Type u_2} {r : ααProp} {s : Set α} {t : Set α} (hs : s.PartiallyWellOrderedOn r) (ht : t.PartiallyWellOrderedOn r) :
        (s t).PartiallyWellOrderedOn r
        @[simp]
        theorem Set.partiallyWellOrderedOn_union {α : Type u_2} {r : ααProp} {s : Set α} {t : Set α} :
        (s t).PartiallyWellOrderedOn r s.PartiallyWellOrderedOn r t.PartiallyWellOrderedOn r
        theorem Set.PartiallyWellOrderedOn.image_of_monotone_on {α : Type u_2} {β : Type u_3} {r : ααProp} {r' : ββProp} {f : αβ} {s : Set α} (hs : s.PartiallyWellOrderedOn r) (hf : a₁s, a₂s, r a₁ a₂r' (f a₁) (f a₂)) :
        (f '' s).PartiallyWellOrderedOn r'
        theorem IsAntichain.finite_of_partiallyWellOrderedOn {α : Type u_2} {r : ααProp} {s : Set α} (ha : IsAntichain r s) (hp : s.PartiallyWellOrderedOn r) :
        s.Finite
        theorem Set.Finite.partiallyWellOrderedOn {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (hs : s.Finite) :
        s.PartiallyWellOrderedOn r
        theorem IsAntichain.partiallyWellOrderedOn_iff {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (hs : IsAntichain r s) :
        s.PartiallyWellOrderedOn r s.Finite
        @[simp]
        theorem Set.partiallyWellOrderedOn_singleton {α : Type u_2} {r : ααProp} [IsRefl α r] (a : α) :
        {a}.PartiallyWellOrderedOn r
        theorem Set.Subsingleton.partiallyWellOrderedOn {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (hs : s.Subsingleton) :
        s.PartiallyWellOrderedOn r
        @[simp]
        theorem Set.partiallyWellOrderedOn_insert {α : Type u_2} {r : ααProp} {s : Set α} {a : α} [IsRefl α r] :
        (insert a s).PartiallyWellOrderedOn r s.PartiallyWellOrderedOn r
        theorem Set.PartiallyWellOrderedOn.insert {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] (h : s.PartiallyWellOrderedOn r) (a : α) :
        (insert a s).PartiallyWellOrderedOn r
        theorem Set.partiallyWellOrderedOn_iff_finite_antichains {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] [IsSymm α r] :
        s.PartiallyWellOrderedOn r ts, IsAntichain r tt.Finite
        theorem Set.PartiallyWellOrderedOn.exists_monotone_subseq {α : Type u_2} {r : ααProp} {s : Set α} [IsRefl α r] [IsTrans α r] (h : s.PartiallyWellOrderedOn r) (f : α) (hf : ∀ (n : ), f n s) :
        ∃ (g : ↪o ), ∀ (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] :
        s.PartiallyWellOrderedOn r ∀ (f : α), (∀ (n : ), f n s)∃ (g : ↪o ), ∀ (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 : s.PartiallyWellOrderedOn r) (ht : t.PartiallyWellOrderedOn r') :
        (s ×ˢ t).PartiallyWellOrderedOn fun (x y : α × β) => r x.1 y.1 r' x.2 y.2
        theorem Set.PartiallyWellOrderedOn.wellFoundedOn {α : Type u_2} {r : ααProp} {s : Set α} [IsPreorder α r] (h : s.PartiallyWellOrderedOn r) :
        s.WellFoundedOn 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
        • s.IsPWO = s.PartiallyWellOrderedOn fun (x1 x2 : α) => x1 x2
        Instances For
          theorem Set.IsPWO.mono {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} (ht : t.IsPWO) :
          s ts.IsPWO
          theorem Set.IsPWO.exists_monotone_subseq {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsPWO) (f : α) (hf : ∀ (n : ), f n s) :
          ∃ (g : ↪o ), Monotone (f g)
          theorem Set.isPWO_iff_exists_monotone_subseq {α : Type u_2} [Preorder α] {s : Set α} :
          s.IsPWO ∀ (f : α), (∀ (n : ), f n s)∃ (g : ↪o ), Monotone (f g)
          theorem Set.IsPWO.isWF {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsPWO) :
          s.IsWF
          theorem Set.IsPWO.prod {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} {t : Set β} (hs : s.IsPWO) (ht : t.IsPWO) :
          (s ×ˢ t).IsPWO
          theorem Set.IsPWO.image_of_monotoneOn {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} (hs : s.IsPWO) {f : αβ} (hf : MonotoneOn f s) :
          (f '' s).IsPWO
          theorem Set.IsPWO.image_of_monotone {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] {s : Set α} (hs : s.IsPWO) {f : αβ} (hf : Monotone f) :
          (f '' s).IsPWO
          theorem Set.IsPWO.union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) :
          (s t).IsPWO
          @[simp]
          theorem Set.isPWO_union {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} :
          (s t).IsPWO s.IsPWO t.IsPWO
          theorem Set.Finite.isPWO {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Finite) :
          s.IsPWO
          @[simp]
          theorem Set.isPWO_of_finite {α : Type u_2} [Preorder α] {s : Set α} [Finite α] :
          s.IsPWO
          @[simp]
          theorem Set.isPWO_singleton {α : Type u_2} [Preorder α] (a : α) :
          {a}.IsPWO
          @[simp]
          theorem Set.isPWO_empty {α : Type u_2} [Preorder α] :
          .IsPWO
          theorem Set.Subsingleton.isPWO {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Subsingleton) :
          s.IsPWO
          @[simp]
          theorem Set.isPWO_insert {α : Type u_2} [Preorder α] {s : Set α} {a : α} :
          (insert a s).IsPWO s.IsPWO
          theorem Set.IsPWO.insert {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsPWO) (a : α) :
          (insert a s).IsPWO
          theorem Set.Finite.isWF {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Finite) :
          s.IsWF
          @[simp]
          theorem Set.isWF_singleton {α : Type u_2} [Preorder α] {a : α} :
          {a}.IsWF
          theorem Set.Subsingleton.isWF {α : Type u_2} [Preorder α] {s : Set α} (hs : s.Subsingleton) :
          s.IsWF
          @[simp]
          theorem Set.isWF_insert {α : Type u_2} [Preorder α] {s : Set α} {a : α} :
          (insert a s).IsWF s.IsWF
          theorem Set.IsWF.insert {α : Type u_2} [Preorder α] {s : Set α} (h : s.IsWF) (a : α) :
          (insert a s).IsWF
          theorem Set.Finite.wellFoundedOn {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} (hs : s.Finite) :
          s.WellFoundedOn r
          @[simp]
          theorem Set.wellFoundedOn_singleton {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {a : α} :
          {a}.WellFoundedOn r
          theorem Set.Subsingleton.wellFoundedOn {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} (hs : s.Subsingleton) :
          s.WellFoundedOn r
          @[simp]
          theorem Set.wellFoundedOn_insert {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} {a : α} :
          (insert a s).WellFoundedOn r s.WellFoundedOn r
          theorem Set.WellFoundedOn.insert {α : Type u_2} {r : ααProp} [IsStrictOrder α r] {s : Set α} (h : s.WellFoundedOn r) (a : α) :
          (insert a s).WellFoundedOn r
          theorem Set.IsWF.isPWO {α : Type u_2} [LinearOrder α] {s : Set α} (hs : s.IsWF) :
          s.IsPWO
          theorem Set.isWF_iff_isPWO {α : Type u_2} [LinearOrder α] {s : Set α} :
          s.IsWF s.IsPWO

          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 α) :
          (↑s).PartiallyWellOrderedOn r
          @[simp]
          theorem Finset.isPWO {α : Type u_2} [Preorder α] (s : Finset α) :
          (↑s).IsPWO
          @[simp]
          theorem Finset.isWF {α : Type u_2} [Preorder α] (s : Finset α) :
          (↑s).IsWF
          @[simp]
          theorem Finset.wellFoundedOn {α : Type u_2} {r : ααProp} [IsStrictOrder α r] (s : Finset α) :
          (↑s).WellFoundedOn r
          theorem Finset.wellFoundedOn_sup {ι : Type u_1} {α : Type u_2} {r : ααProp} [IsStrictOrder α r] (s : Finset ι) {f : ιSet α} :
          (s.sup f).WellFoundedOn r is, (f i).WellFoundedOn r
          theorem Finset.partiallyWellOrderedOn_sup {ι : Type u_1} {α : Type u_2} {r : ααProp} (s : Finset ι) {f : ιSet α} :
          (s.sup f).PartiallyWellOrderedOn r is, (f i).PartiallyWellOrderedOn r
          theorem Finset.isWF_sup {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          (s.sup f).IsWF is, (f i).IsWF
          theorem Finset.isPWO_sup {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          (s.sup f).IsPWO is, (f i).IsPWO
          @[simp]
          theorem Finset.wellFoundedOn_bUnion {ι : Type u_1} {α : Type u_2} {r : ααProp} [IsStrictOrder α r] (s : Finset ι) {f : ιSet α} :
          (⋃ is, f i).WellFoundedOn r is, (f i).WellFoundedOn r
          @[simp]
          theorem Finset.partiallyWellOrderedOn_bUnion {ι : Type u_1} {α : Type u_2} {r : ααProp} (s : Finset ι) {f : ιSet α} :
          (⋃ is, f i).PartiallyWellOrderedOn r is, (f i).PartiallyWellOrderedOn r
          @[simp]
          theorem Finset.isWF_bUnion {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          (⋃ is, f i).IsWF is, (f i).IsWF
          @[simp]
          theorem Finset.isPWO_bUnion {ι : Type u_1} {α : Type u_2} [Preorder α] (s : Finset ι) {f : ιSet α} :
          (⋃ is, f i).IsPWO is, (f i).IsPWO
          noncomputable def Set.IsWF.min {α : Type u_2} [Preorder α] {s : Set α} (hs : s.IsWF) (hn : s.Nonempty) :
          α

          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 : s.IsWF) (hn : s.Nonempty) :
            hs.min hn s
            theorem Set.IsWF.not_lt_min {α : Type u_2} [Preorder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty) (ha : a s) :
            ¬a < hs.min hn
            theorem Set.IsWF.min_of_subset_not_lt_min {α : Type u_2} [Preorder α] {s : Set α} {t : Set α} {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty} (hst : s t) :
            ¬hs.min hsn < ht.min htn
            @[simp]
            theorem Set.isWF_min_singleton {α : Type u_2} [Preorder α] (a : α) {hs : {a}.IsWF} {hn : {a}.Nonempty} :
            hs.min hn = a
            theorem Set.IsWF.min_le {α : Type u_2} [LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty) (ha : a s) :
            hs.min hn a
            theorem Set.IsWF.le_min_iff {α : Type u_2} [LinearOrder α] {s : Set α} {a : α} (hs : s.IsWF) (hn : s.Nonempty) :
            a hs.min hn bs, a b
            theorem Set.IsWF.min_le_min_of_subset {α : Type u_2} [LinearOrder α] {s : Set α} {t : Set α} {hs : s.IsWF} {hsn : s.Nonempty} {ht : t.IsWF} {htn : t.Nonempty} (hst : s t) :
            ht.min htn hs.min hsn
            theorem Set.IsWF.min_union {α : Type u_2} [LinearOrder α] {s : Set α} {t : Set α} (hs : s.IsWF) (hsn : s.Nonempty) (ht : t.IsWF) (htn : t.Nonempty) :
            .min = min (hs.min hsn) (ht.min htn)
            theorem BddBelow.wellFoundedOn_lt {α : Type u_2} {s : Set α} [Preorder α] [LocallyFiniteOrder α] :
            BddBelow ss.WellFoundedOn fun (x1 x2 : α) => x1 < x2
            theorem BddAbove.wellFoundedOn_gt {α : Type u_2} {s : Set α} [Preorder α] [LocallyFiniteOrder α] :
            BddAbove ss.WellFoundedOn fun (x1 x2 : α) => x1 > x2
            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
              theorem Set.PartiallyWellOrderedOn.iff_forall_not_isBadSeq {α : Type u_2} (r : ααProp) (s : Set α) :
              s.PartiallyWellOrderedOn r ∀ (f : α), ¬Set.PartiallyWellOrderedOn.IsBadSeq r s f
              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 < n, f 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 α) :
                  (∃ (f : α), Set.PartiallyWellOrderedOn.IsBadSeq r s f)∃ (f : α), Set.PartiallyWellOrderedOn.IsBadSeq r s f ∀ (n : ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f
                  theorem Set.PartiallyWellOrderedOn.iff_not_exists_isMinBadSeq {α : Type u_2} {r : ααProp} (rk : α) {s : Set α} :
                  s.PartiallyWellOrderedOn r ¬∃ (f : α), Set.PartiallyWellOrderedOn.IsBadSeq r s f ∀ (n : ), Set.PartiallyWellOrderedOn.IsMinBadSeq r rk s n f
                  theorem Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂ {α : Type u_2} (r : ααProp) [IsRefl α r] [IsTrans α r] {s : Set α} (h : s.PartiallyWellOrderedOn r) :
                  {l : List α | xl, x s}.PartiallyWellOrderedOn (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 Set.PartiallyWellOrderedOn.subsetProdLex {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} (hα : ((fun (x : Lex (α × β)) => (ofLex x).1) '' s).IsPWO) (hβ : ∀ (a : α), {y : β | toLex (a, y) s}.IsPWO) :
                  s.IsPWO
                  theorem Set.PartiallyWellOrderedOn.imageProdLex {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} (hαβ : s.IsPWO) :
                  ((fun (x : Lex (α × β)) => (ofLex x).1) '' s).IsPWO
                  theorem Set.PartiallyWellOrderedOn.fiberProdLex {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} (hαβ : s.IsPWO) (a : α) :
                  {y : β | toLex (a, y) s}.IsPWO
                  theorem Set.PartiallyWellOrderedOn.ProdLex_iff {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] {s : Set (Lex (α × β))} :
                  s.IsPWO ((fun (x : Lex (α × β)) => (ofLex x).1) '' s).IsPWO ∀ (a : α), {y : β | toLex (a, y) s}.IsPWO
                  theorem WellFounded.isWF {α : Type u_2} [LT α] (h : WellFounded fun (x1 x2 : α) => x1 < x2) (s : Set α) :
                  s.IsWF
                  theorem Pi.isPWO {ι : Type u_1} {α : ιType u_6} [(i : ι) → LinearOrder (α i)] [∀ (i : ι), IsWellOrder (α i) fun (x1 x2 : α i) => x1 < x2] [Finite ι] (s : Set ((i : ι) → α i)) :
                  s.IsPWO

                  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 : α), (f ⁻¹' {a}).WellFoundedOn ( 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α : s.WellFoundedOn ( on f)) (hβ : ∀ (a : α), (s f ⁻¹' {a}).WellFoundedOn ( on g)) :
                  s.WellFoundedOn (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 : ι), (f ⁻¹' {i}).WellFoundedOn ( i on g i)) :
                  WellFounded (Sigma.Lex on fun (c : γ) => f c, 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ι : s.WellFoundedOn ( on f)) (hπ : ∀ (i : ι), (s f ⁻¹' {i}).WellFoundedOn ( i on g i)) :
                  s.WellFoundedOn (Sigma.Lex on fun (c : γ) => f c, g (f c) c)