# Well-founded sets #

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

## Main Definitions #

• Set.WellFoundedOn s r indicates that the relation r is well-founded when restricted to the set s.
• Set.IsWF s indicates that < is well-founded when restricted to s.
• Set.PartiallyWellOrderedOn s r indicates that the relation r is partially well-ordered (also known as well quasi-ordered) when restricted to the set s.
• Set.IsPWO s indicates that any infinite sequence of elements in s contains an infinite monotone subsequence. Note that this is equivalent to containing only two comparable elements.

## Main Results #

• Higman's Lemma, Set.PartiallyWellOrderedOn.partiallyWellOrderedOn_sublistForall₂, shows that if r is partially well-ordered on s, then List.SublistForall₂ is partially well-ordered on the set of lists of elements of s. The result was originally published by Higman, but this proof more closely follows Nash-Williams.
• Set.wellFoundedOn_iff relates well_founded_on to the well-foundedness of a relation on the original type, to avoid dealing with subtypes.
• Set.IsWF.mono shows that a subset of a well-founded subset is well-founded.
• Set.IsWF.union shows that the union of two well-founded subsets is well-founded.
• Finset.isWF shows that all Finsets are well-founded.

## 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
theorem WellFounded.wellFoundedOn {α : Type u_2} {r : ααProp} {s : Set α} :
s.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 : α | }.WellFoundedOn r, {b : α | }.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} [] {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} [] {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} [] {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} [] {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} [] {s : Set α} {t : Set α} (hs : s.IsWF) (ht : t.IsWF) :
(s t).IsWF
@[simp]
theorem Set.isWF_union {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).IsWF s.IsWF t.IsWF
theorem Set.isWF_iff_no_descending_seq {α : Type u_2} [] {s : Set α} :
s.IsWF ∀ (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 : ) (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 : ) :
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, t.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 : ), ∀ (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 : ), ∀ (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 α} [] (h : s.PartiallyWellOrderedOn r) :
s.WellFoundedOn fun (a b : α) => r a b ¬r b a
def Set.IsPWO {α : Type u_2} [] (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} [] {s : Set α} {t : Set α} (ht : t.IsPWO) :
s ts.IsPWO
theorem Set.IsPWO.exists_monotone_subseq {α : Type u_2} [] {s : Set α} (h : s.IsPWO) (f : α) (hf : ∀ (n : ), f n s) :
∃ (g : ), Monotone (f g)
theorem Set.isPWO_iff_exists_monotone_subseq {α : Type u_2} [] {s : Set α} :
s.IsPWO ∀ (f : α), (∀ (n : ), f n s)∃ (g : ), Monotone (f g)
theorem Set.IsPWO.isWF {α : Type u_2} [] {s : Set α} (h : s.IsPWO) :
s.IsWF
theorem Set.IsPWO.prod {α : Type u_2} {β : Type u_3} [] [] {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} [] [] {s : Set α} (hs : s.IsPWO) {f : αβ} (hf : ) :
(f '' s).IsPWO
theorem Set.IsPWO.image_of_monotone {α : Type u_2} {β : Type u_3} [] [] {s : Set α} (hs : s.IsPWO) {f : αβ} (hf : ) :
(f '' s).IsPWO
theorem Set.IsPWO.union {α : Type u_2} [] {s : Set α} {t : Set α} (hs : s.IsPWO) (ht : t.IsPWO) :
(s t).IsPWO
@[simp]
theorem Set.isPWO_union {α : Type u_2} [] {s : Set α} {t : Set α} :
(s t).IsPWO s.IsPWO t.IsPWO
theorem Set.Finite.isPWO {α : Type u_2} [] {s : Set α} (hs : s.Finite) :
s.IsPWO
@[simp]
theorem Set.isPWO_of_finite {α : Type u_2} [] {s : Set α} [] :
s.IsPWO
@[simp]
theorem Set.isPWO_singleton {α : Type u_2} [] (a : α) :
{a}.IsPWO
@[simp]
theorem Set.isPWO_empty {α : Type u_2} [] :
.IsPWO
theorem Set.Subsingleton.isPWO {α : Type u_2} [] {s : Set α} (hs : s.Subsingleton) :
s.IsPWO
@[simp]
theorem Set.isPWO_insert {α : Type u_2} [] {s : Set α} {a : α} :
(insert a s).IsPWO s.IsPWO
theorem Set.IsPWO.insert {α : Type u_2} [] {s : Set α} (h : s.IsPWO) (a : α) :
(insert a s).IsPWO
theorem Set.Finite.isWF {α : Type u_2} [] {s : Set α} (hs : s.Finite) :
s.IsWF
@[simp]
theorem Set.isWF_singleton {α : Type u_2} [] {a : α} :
{a}.IsWF
theorem Set.Subsingleton.isWF {α : Type u_2} [] {s : Set α} (hs : s.Subsingleton) :
s.IsWF
@[simp]
theorem Set.isWF_insert {α : Type u_2} [] {s : Set α} {a : α} :
(insert a s).IsWF s.IsWF
theorem Set.IsWF.insert {α : Type u_2} [] {s : Set α} (h : s.IsWF) (a : α) :
(insert a s).IsWF
theorem Set.Finite.wellFoundedOn {α : Type u_2} {r : ααProp} [] {s : Set α} (hs : s.Finite) :
s.WellFoundedOn r
@[simp]
theorem Set.wellFoundedOn_singleton {α : Type u_2} {r : ααProp} [] {a : α} :
{a}.WellFoundedOn r
theorem Set.Subsingleton.wellFoundedOn {α : Type u_2} {r : ααProp} [] {s : Set α} (hs : s.Subsingleton) :
s.WellFoundedOn r
@[simp]
theorem Set.wellFoundedOn_insert {α : Type u_2} {r : ααProp} [] {s : Set α} {a : α} :
(insert a s).WellFoundedOn r s.WellFoundedOn r
theorem Set.WellFoundedOn.insert {α : Type u_2} {r : ααProp} [] {s : Set α} (h : s.WellFoundedOn r) (a : α) :
(insert a s).WellFoundedOn r
theorem Set.IsWF.isPWO {α : Type u_2} [] {s : Set α} (hs : s.IsWF) :
s.IsPWO
theorem Set.isWF_iff_isPWO {α : Type u_2} [] {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 : ) :
(↑s).PartiallyWellOrderedOn r
@[simp]
theorem Finset.isPWO {α : Type u_2} [] (s : ) :
(↑s).IsPWO
@[simp]
theorem Finset.isWF {α : Type u_2} [] (s : ) :
(↑s).IsWF
@[simp]
theorem Finset.wellFoundedOn {α : Type u_2} {r : ααProp} [] (s : ) :
(↑s).WellFoundedOn r
theorem Finset.wellFoundedOn_sup {ι : Type u_1} {α : Type u_2} {r : ααProp} [] (s : ) {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 : ) {f : ιSet α} :
(s.sup f).PartiallyWellOrderedOn r is, (f i).PartiallyWellOrderedOn r
theorem Finset.isWF_sup {ι : Type u_1} {α : Type u_2} [] (s : ) {f : ιSet α} :
(s.sup f).IsWF is, (f i).IsWF
theorem Finset.isPWO_sup {ι : Type u_1} {α : Type u_2} [] (s : ) {f : ιSet α} :
(s.sup f).IsPWO is, (f i).IsPWO
@[simp]
theorem Finset.wellFoundedOn_bUnion {ι : Type u_1} {α : Type u_2} {r : ααProp} [] (s : ) {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 : ) {f : ιSet α} :
(⋃ is, f i).PartiallyWellOrderedOn r is, (f i).PartiallyWellOrderedOn r
@[simp]
theorem Finset.isWF_bUnion {ι : Type u_1} {α : Type u_2} [] (s : ) {f : ιSet α} :
(⋃ is, f i).IsWF is, (f i).IsWF
@[simp]
theorem Finset.isPWO_bUnion {ι : Type u_1} {α : Type u_2} [] (s : ) {f : ιSet α} :
(⋃ is, f i).IsPWO is, (f i).IsPWO
noncomputable def Set.IsWF.min {α : Type u_2} [] {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} [] {s : Set α} (hs : s.IsWF) (hn : s.Nonempty) :
hs.min hn s
theorem Set.IsWF.not_lt_min {α : Type u_2} [] {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} [] {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} [] (a : α) {hs : {a}.IsWF} {hn : {a}.Nonempty} :
hs.min hn = a
theorem Set.IsWF.min_le {α : Type u_2} [] {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} [] {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} [] {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} [] {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 α} [] :
s.WellFoundedOn fun (x1 x2 : α) => x1 < x2
theorem BddAbove.wellFoundedOn_gt {α : Type u_2} {s : Set α} [] :
s.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 : α),
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
• = ∀ (g : α), (∀ m < n, f m = g m)rk (g n) < rk (f n)
Instances For
noncomputable def Set.PartiallyWellOrderedOn.minBadSeqOfBadSeq {α : Type u_2} (r : ααProp) (rk : α) (s : Set α) (n : ) (f : α) (hf : ) :
{ g : α // (∀ m < n, f m = g m) }

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 : α), )∃ (f : α), ∀ (n : ),
theorem Set.PartiallyWellOrderedOn.iff_not_exists_isMinBadSeq {α : Type u_2} {r : ααProp} (rk : α) {s : Set α} :
s.PartiallyWellOrderedOn r ¬∃ (f : α), ∀ (n : ),
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

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} [] [] {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} [] [] {s : Set (Lex (α × β))} (hαβ : s.IsPWO) :
((fun (x : Lex (α × β)) => (ofLex x).1) '' s).IsPWO
theorem Set.PartiallyWellOrderedOn.fiberProdLex {α : Type u_2} {β : Type u_3} [] [] {s : Set (Lex (α × β))} (hαβ : s.IsPWO) (a : α) :
{y : β | toLex (a, y) s}.IsPWO
theorem Set.PartiallyWellOrderedOn.ProdLex_iff {α : Type u_2} {β : Type u_3} [] [] {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] [] (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)