# mathlibdocumentation

order.well_founded_set

# Well-founded sets #

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)
@[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 sr z yP 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.subset {α : Type u_2} {r : α → α → Prop} {s t : set α} (h : t.well_founded_on r) (hst : s t) :
@[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
• = ∀ (f : → α), (∀ (n : ), f n s)(∃ (m n : ), m < n r (f m) (f n))
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₂ sr 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 nr (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 nr (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) :
∃ (g : ↪o ), monotone (f g)
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 sa 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
• = ∀ (g : → α), (∀ (m : ), m < nf m = g m)rk (g n) < rk (f n)
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 < nf 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
• hf = and.dcases_on _ (λ (h1 : ∀ (m : ), m < nf m = m) (right : rk n) = nat.find _), right.dcases_on (λ (h2 : (h3 : rk n) = nat.find _), , _⟩))
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 lx 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.