# mathlib3documentation

order.well_founded_set

# Well-founded sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main Definitions #

• set.well_founded_on s r indicates that the relation r is well-founded when restricted to the set s.
• set.is_wf s indicates that < is well-founded when restricted to s.
• set.partially_well_ordered_on s r indicates that the relation r is partially well-ordered (also known as well quasi-ordered) when restricted to the set s.
• set.is_pwo 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.partially_well_ordered_on.partially_well_ordered_on_sublist_forall₂, shows that if r is partially well-ordered on s, then list.sublist_forall₂ 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.well_founded_on_iff relates well_founded_on to the well-foundedness of a relation on the original type, to avoid dealing with subtypes.
• set.is_wf.mono shows that a subset of a well-founded subset is well-founded.
• set.is_wf.union shows that the union of two well-founded subsets is well-founded.
• finset.is_wf 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.well_founded_on {α : Type u_2} (s : set α) (r : α α Prop) :
Prop

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

Equations
@[simp]
theorem set.well_founded_on_empty {α : Type u_2} (r : α α Prop) :
theorem set.well_founded_on_iff {α : Type u_2} {r : α α Prop} {s : set α} :
well_founded (λ (a b : α), r a b a s b s)
@[simp]
theorem set.well_founded_on_univ {α : Type u_2} {r : α α Prop} :
theorem well_founded.well_founded_on {α : Type u_2} {r : α α Prop} {s : set α} :
@[simp]
theorem set.well_founded_on_range {α : Type u_2} {β : Type u_3} {r : α α Prop} {f : β α} :
@[simp]
theorem set.well_founded_on_image {α : Type u_2} {β : Type u_3} {r : α α Prop} {f : β α} {s : set β} :
@[protected]
theorem set.well_founded_on.induction {α : Type u_2} {r : α α Prop} {s : set α} {x : α} (hs : s.well_founded_on r) (hx : x s) {P : α Prop} (hP : (y : α), y s ( (z : α), z s r z y P z) P y) :
P x
@[protected]
theorem set.well_founded_on.mono {α : Type u_2} {r r' : α α Prop} {s t : set α} (h : t.well_founded_on r') (hle : r r') (hst : s t) :
theorem set.well_founded_on.mono' {α : Type u_2} {r r' : α α Prop} {s : set α} (h : (a : α), a s (b : α), b s r' a b r a b) :
theorem set.well_founded_on.subset {α : Type u_2} {r : α α Prop} {s t : set α} (h : t.well_founded_on r) (hst : s t) :
theorem set.well_founded_on.acc_iff_well_founded_on {α : Type u_1} {r : α α Prop} {a : α} :
[acc r a, {b : α | a}.well_founded_on r, {b : α | a}.well_founded_on 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).

@[protected, instance]
def set.is_strict_order.subset {α : Type u_2} {r : α α Prop} [ r] {s : set α} :
(λ (a b : α), r a b a s b s)
theorem set.well_founded_on_iff_no_descending_seq {α : Type u_2} {r : α α Prop} [ r] {s : set α} :
(f : gt ↪r r), ¬ (n : ), f n s
theorem set.well_founded_on.union {α : Type u_2} {r : α α Prop} [ r] {s t : set α} (hs : s.well_founded_on r) (ht : t.well_founded_on r) :
@[simp]
theorem set.well_founded_on_union {α : Type u_2} {r : α α Prop} [ r] {s t : set α} :

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

def set.is_wf {α : Type u_2} [has_lt α] (s : set α) :
Prop

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

Equations
@[simp]
theorem set.is_wf_empty {α : Type u_2} [has_lt α] :
theorem set.is_wf_univ_iff {α : Type u_2} [has_lt α] :
theorem set.is_wf.mono {α : Type u_2} [has_lt α] {s t : set α} (h : t.is_wf) (st : s t) :
@[protected]
theorem set.is_wf.union {α : Type u_2} [preorder α] {s t : set α} (hs : s.is_wf) (ht : t.is_wf) :
(s t).is_wf
@[simp]
theorem set.is_wf_union {α : Type u_2} [preorder α] {s t : set α} :
theorem set.is_wf_iff_no_descending_seq {α : Type u_2} [preorder α] {s : set α} :
s.is_wf (f : α), (¬ (n : ), f 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 is_antichain) is finite, see set.partially_well_ordered_on_iff_finite_antichains.

def set.partially_well_ordered_on {α : Type u_2} (s : set α) (r : α α Prop) :
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
theorem set.partially_well_ordered_on.mono {α : Type u_2} {r : α α Prop} {s t : set α} (ht : t.partially_well_ordered_on r) (h : s t) :
@[simp]
theorem set.partially_well_ordered_on_empty {α : Type u_2} (r : α α Prop) :
theorem set.partially_well_ordered_on.union {α : Type u_2} {r : α α Prop} {s t : set α} (hs : s.partially_well_ordered_on r) (ht : t.partially_well_ordered_on r) :
@[simp]
theorem set.partially_well_ordered_on_union {α : Type u_2} {r : α α Prop} {s t : set α} :
theorem set.partially_well_ordered_on.image_of_monotone_on {α : Type u_2} {β : Type u_3} {r : α α Prop} {r' : β β Prop} {f : α β} {s : set α} (hs : s.partially_well_ordered_on r) (hf : (a₁ : α), a₁ s (a₂ : α), a₂ s r a₁ a₂ r' (f a₁) (f a₂)) :
theorem is_antichain.finite_of_partially_well_ordered_on {α : Type u_2} {r : α α Prop} {s : set α} (ha : s) (hp : s.partially_well_ordered_on r) :
@[protected]
theorem set.finite.partially_well_ordered_on {α : Type u_2} {r : α α Prop} {s : set α} [ r] (hs : s.finite) :
theorem is_antichain.partially_well_ordered_on_iff {α : Type u_2} {r : α α Prop} {s : set α} [ r] (hs : s) :
@[simp]
theorem set.partially_well_ordered_on_singleton {α : Type u_2} {r : α α Prop} [ r] (a : α) :
@[simp]
theorem set.partially_well_ordered_on_insert {α : Type u_2} {r : α α Prop} {s : set α} {a : α} [ r] :
@[protected]
theorem set.partially_well_ordered_on.insert {α : Type u_2} {r : α α Prop} {s : set α} [ r] (h : s.partially_well_ordered_on r) (a : α) :
theorem set.partially_well_ordered_on_iff_finite_antichains {α : Type u_2} {r : α α Prop} {s : set α} [ r] [ r] :
(t : set α), t s t t.finite
theorem set.partially_well_ordered_on.exists_monotone_subseq {α : Type u_2} {r : α α Prop} {s : set α} [ r] [ r] (h : s.partially_well_ordered_on r) (f : α) (hf : (n : ), f n s) :
(g : ↪o ), (m n : ), m n r (f (g m)) (f (g n))
theorem set.partially_well_ordered_on_iff_exists_monotone_subseq {α : Type u_2} {r : α α Prop} {s : set α} [ r] [ r] :
(f : α), ( (n : ), f n s) ( (g : ↪o ), (m n : ), m n r (f (g m)) (f (g n)))
@[protected]
theorem set.partially_well_ordered_on.prod {α : Type u_2} {β : Type u_3} {r : α α Prop} {r' : β β Prop} {s : set α} [ r] [ r] {t : set β} (hs : s.partially_well_ordered_on r) (ht : t.partially_well_ordered_on r') :
(s ×ˢ t).partially_well_ordered_on (λ (x y : α × β), r x.fst y.fst r' x.snd y.snd)
theorem set.partially_well_ordered_on.well_founded_on {α : Type u_2} {r : α α Prop} {s : set α} [ r] (h : s.partially_well_ordered_on r) :
s.well_founded_on (λ (a b : α), r a b ¬r b a)
def set.is_pwo {α : Type u_2} [preorder α] (s : set α) :
Prop

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
theorem set.is_pwo.mono {α : Type u_2} [preorder α] {s t : set α} (ht : t.is_pwo) :
s t s.is_pwo
theorem set.is_pwo.exists_monotone_subseq {α : Type u_2} [preorder α] {s : set α} (h : s.is_pwo) (f : α) (hf : (n : ), f n s) :
theorem set.is_pwo_iff_exists_monotone_subseq {α : Type u_2} [preorder α] {s : set α} :
s.is_pwo (f : α), ( (n : ), f n s) ( (g : ↪o ), monotone (f g))
@[protected]
theorem set.is_pwo.is_wf {α : Type u_2} [preorder α] {s : set α} (h : s.is_pwo) :
theorem set.is_pwo.prod {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {s : set α} {t : set β} (hs : s.is_pwo) (ht : t.is_pwo) :
(s ×ˢ t).is_pwo
theorem set.is_pwo.image_of_monotone_on {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {s : set α} (hs : s.is_pwo) {f : α β} (hf : s) :
(f '' s).is_pwo
theorem set.is_pwo.image_of_monotone {α : Type u_2} {β : Type u_3} [preorder α] [preorder β] {s : set α} (hs : s.is_pwo) {f : α β} (hf : monotone f) :
(f '' s).is_pwo
@[protected]
theorem set.is_pwo.union {α : Type u_2} [preorder α] {s t : set α} (hs : s.is_pwo) (ht : t.is_pwo) :
(s t).is_pwo
@[simp]
theorem set.is_pwo_union {α : Type u_2} [preorder α] {s t : set α} :
@[protected]
theorem set.finite.is_pwo {α : Type u_2} [preorder α] {s : set α} (hs : s.finite) :
@[simp]
theorem set.is_pwo_of_finite {α : Type u_2} [preorder α] {s : set α} [finite α] :
@[simp]
theorem set.is_pwo_singleton {α : Type u_2} [preorder α] (a : α) :
{a}.is_pwo
@[simp]
theorem set.is_pwo_empty {α : Type u_2} [preorder α] :
@[protected]
theorem set.subsingleton.is_pwo {α : Type u_2} [preorder α] {s : set α} (hs : s.subsingleton) :
@[simp]
theorem set.is_pwo_insert {α : Type u_2} [preorder α] {s : set α} {a : α} :
@[protected]
theorem set.is_pwo.insert {α : Type u_2} [preorder α] {s : set α} (h : s.is_pwo) (a : α) :
s).is_pwo
@[protected]
theorem set.finite.is_wf {α : Type u_2} [preorder α] {s : set α} (hs : s.finite) :
@[simp]
theorem set.is_wf_singleton {α : Type u_2} [preorder α] {a : α} :
{a}.is_wf
@[protected]
theorem set.subsingleton.is_wf {α : Type u_2} [preorder α] {s : set α} (hs : s.subsingleton) :
@[simp]
theorem set.is_wf_insert {α : Type u_2} [preorder α] {s : set α} {a : α} :
theorem set.is_wf.insert {α : Type u_2} [preorder α] {s : set α} (h : s.is_wf) (a : α) :
s).is_wf
@[protected]
theorem set.finite.well_founded_on {α : Type u_2} {r : α α Prop} [ r] {s : set α} (hs : s.finite) :
@[simp]
theorem set.well_founded_on_singleton {α : Type u_2} {r : α α Prop} [ r] {a : α} :
@[protected]
theorem set.subsingleton.well_founded_on {α : Type u_2} {r : α α Prop} [ r] {s : set α} (hs : s.subsingleton) :
@[simp]
theorem set.well_founded_on_insert {α : Type u_2} {r : α α Prop} [ r] {s : set α} {a : α} :
r
theorem set.well_founded_on.insert {α : Type u_2} {r : α α Prop} [ r] {s : set α} (h : s.well_founded_on r) (a : α) :
r
@[protected]
theorem set.is_wf.is_pwo {α : Type u_2} [linear_order α] {s : set α} (hs : s.is_wf) :
theorem set.is_wf_iff_is_pwo {α : Type u_2} [linear_order α] {s : set α} :

In a linear order, the predicates set.is_wf and set.is_pwo are equivalent.

@[protected, simp]
theorem finset.partially_well_ordered_on {α : Type u_2} {r : α α Prop} [ r] (s : finset α) :
@[protected, simp]
theorem finset.is_pwo {α : Type u_2} [preorder α] (s : finset α) :
@[protected, simp]
theorem finset.is_wf {α : Type u_2} [preorder α] (s : finset α) :
@[protected, simp]
theorem finset.well_founded_on {α : Type u_2} {r : α α Prop} [ r] (s : finset α) :
theorem finset.well_founded_on_sup {ι : Type u_1} {α : Type u_2} {r : α α Prop} [ r] (s : finset ι) {f : ι set α} :
(s.sup f).well_founded_on r (i : ι), i s (f i).well_founded_on r
theorem finset.partially_well_ordered_on_sup {ι : Type u_1} {α : Type u_2} {r : α α Prop} (s : finset ι) {f : ι set α} :
(s.sup f).partially_well_ordered_on r (i : ι), i s r
theorem finset.is_wf_sup {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι set α} :
(s.sup f).is_wf (i : ι), i s (f i).is_wf
theorem finset.is_pwo_sup {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι set α} :
(s.sup f).is_pwo (i : ι), i s (f i).is_pwo
@[simp]
theorem finset.well_founded_on_bUnion {ι : Type u_1} {α : Type u_2} {r : α α Prop} [ r] (s : finset ι) {f : ι set α} :
( (i : ι) (H : i s), f i).well_founded_on r (i : ι), i s (f i).well_founded_on r
@[simp]
theorem finset.partially_well_ordered_on_bUnion {ι : Type u_1} {α : Type u_2} {r : α α Prop} (s : finset ι) {f : ι set α} :
( (i : ι) (H : i s), f i).partially_well_ordered_on r (i : ι), i s r
@[simp]
theorem finset.is_wf_bUnion {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι set α} :
( (i : ι) (H : i s), f i).is_wf (i : ι), i s (f i).is_wf
@[simp]
theorem finset.is_pwo_bUnion {ι : Type u_1} {α : Type u_2} [preorder α] (s : finset ι) {f : ι set α} :
( (i : ι) (H : i s), f i).is_pwo (i : ι), i s (f i).is_pwo
noncomputable def set.is_wf.min {α : Type u_2} [preorder α] {s : set α} (hs : s.is_wf) (hn : s.nonempty) :
α

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

Equations
theorem set.is_wf.min_mem {α : Type u_2} [preorder α] {s : set α} (hs : s.is_wf) (hn : s.nonempty) :
hs.min hn s
theorem set.is_wf.not_lt_min {α : Type u_2} [preorder α] {s : set α} {a : α} (hs : s.is_wf) (hn : s.nonempty) (ha : a s) :
¬a < hs.min hn
@[simp]
theorem set.is_wf_min_singleton {α : Type u_2} [preorder α] (a : α) {hs : {a}.is_wf} {hn : {a}.nonempty} :
hs.min hn = a
theorem set.is_wf.min_le {α : Type u_2} [linear_order α] {s : set α} {a : α} (hs : s.is_wf) (hn : s.nonempty) (ha : a s) :
hs.min hn a
theorem set.is_wf.le_min_iff {α : Type u_2} [linear_order α] {s : set α} {a : α} (hs : s.is_wf) (hn : s.nonempty) :
a hs.min hn (b : α), b s a b
theorem set.is_wf.min_le_min_of_subset {α : Type u_2} [linear_order α] {s t : set α} {hs : s.is_wf} {hsn : s.nonempty} {ht : t.is_wf} {htn : t.nonempty} (hst : s t) :
ht.min htn hs.min hsn
theorem set.is_wf.min_union {α : Type u_2} [linear_order α] {s t : set α} (hs : s.is_wf) (hsn : s.nonempty) (ht : t.is_wf) (htn : t.nonempty) :
_.min _ = linear_order.min (hs.min hsn) (ht.min htn)
def set.partially_well_ordered_on.is_bad_seq {α : Type u_2} (r : α α Prop) (s : set α) (f : α) :
Prop

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
theorem set.partially_well_ordered_on.iff_forall_not_is_bad_seq {α : Type u_2} (r : α α Prop) (s : set α) :
(f : α),
def set.partially_well_ordered_on.is_min_bad_seq {α : Type u_2} (r : α α Prop) (rk : α ) (s : set α) (n : ) (f : α) :
Prop

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

Equations
noncomputable def set.partially_well_ordered_on.min_bad_seq_of_bad_seq {α : Type u_2} (r : α α Prop) (rk : α ) (s : set α) (n : ) (f : α) (hf : f) :
{g // ( (m : ), 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
theorem set.partially_well_ordered_on.exists_min_bad_of_exists_bad {α : Type u_2} (r : α α Prop) (rk : α ) (s : set α) :
( (f : α), ( (f : α), (n : ), f)
theorem set.partially_well_ordered_on.iff_not_exists_is_min_bad_seq {α : Type u_2} {r : α α Prop} (rk : α ) {s : set α} :
¬ (f : α), (n : ),
theorem set.partially_well_ordered_on.partially_well_ordered_on_sublist_forall₂ {α : Type u_2} (r : α α Prop) [ r] [ r] {s : set α} (h : s.partially_well_ordered_on r) :
{l : list α | (x : α), x l x s}.partially_well_ordered_on

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

theorem well_founded.is_wf {α : Type u_2} [has_lt α] (s : set α) :
theorem pi.is_pwo {ι : Type u_1} {α : ι Type u_2} [Π (i : ι), linear_order (α i)] [ (i : ι), is_well_order (α i) has_lt.lt] [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.partially_well_ordered_on instead of set.is_pwo.

theorem well_founded.prod_lex_of_well_founded_on_fiber {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α α Prop} {rβ : β β Prop} {f : γ α} {g : γ β} (hα : well_founded (rα on f)) (hβ : (a : α), (f ⁻¹' {a}).well_founded_on (rβ on g)) :
well_founded (prod.lex on λ (c : γ), (f c, g c))

Stronger version of prod.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.well_founded_on.prod_lex_of_well_founded_on_fiber {α : Type u_2} {β : Type u_3} {γ : Type u_4} {rα : α α Prop} {rβ : β β Prop} {f : γ α} {g : γ β} {s : set γ} (hα : s.well_founded_on (rα on f)) (hβ : (a : α), (s f ⁻¹' {a}).well_founded_on (rβ on g)) :
s.well_founded_on (prod.lex on λ (c : γ), (f c, g c))
theorem well_founded.sigma_lex_of_well_founded_on_fiber {ι : Type u_1} {γ : Type u_4} {π : ι Type u_5} {rι : ι ι Prop} {rπ : Π (i : ι), π i π i Prop} {f : γ ι} {g : Π (i : ι), γ π i} (hι : well_founded (rι on f)) (hπ : (i : ι), (f ⁻¹' {i}).well_founded_on (rπ i on g i)) :
well_founded (sigma.lex on λ (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.well_founded_on.sigma_lex_of_well_founded_on_fiber {ι : Type u_1} {γ : Type u_4} {π : ι Type u_5} {rι : ι ι Prop} {rπ : Π (i : ι), π i π i Prop} {f : γ ι} {g : Π (i : ι), γ π i} {s : set γ} (hι : s.well_founded_on (rι on f)) (hπ : (i : ι), (s f ⁻¹' {i}).well_founded_on (rπ i on g i)) :
s.well_founded_on (sigma.lex on λ (c : γ), f c, g (f c) c⟩)