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 rindicates that the relation
ris well-founded when restricted to the set
set.is_wf sindicates that
<is well-founded when restricted to
set.partially_well_ordered_on s rindicates that the relation
ris partially well-ordered (also known as well quasi-ordered) when restricted to the set
set.is_pwo sindicates that any infinite sequence of elements in
scontains 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
ris partially well-ordered on
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.
well_founded_onto the well-foundedness of a relation on the original type, to avoid dealing with subtypes.
set.is_wf.monoshows that a subset of a well-founded subset is well-founded.
set.is_wf.unionshows that the union of two well-founded subsets is well-founded.
finset.is_wfshows that all
finsets are well-founded.
s is partial well ordered iff it has no infinite descending chain or antichain.
Relations well-founded on sets #
s.well_founded_on r indicates that the relation
r is well-founded when restricted to
- s.well_founded_on r = well_founded (λ (a b : ↥s), r ↑a ↑b)
a is accessible under the relation
r is well-founded on the downward transitive
a or not).
Sets well-founded w.r.t. the strict inequality #
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
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
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).
In a linear order, the predicates
set.is_pwo are equivalent.
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
This indicates that every bad sequence
g that agrees with
f on the first
rk (f n) ≤ rk (g n).
Given a bad sequence
f, this constructs a bad sequence that agrees with
f on the first
terms and is minimal at
- set.partially_well_ordered_on.min_bad_seq_of_bad_seq r rk s n f hf = and.dcases_on _ (λ (h1 : ∀ (m : ℕ), m < n → f m = classical.some _ m) (right : set.partially_well_ordered_on.is_bad_seq r s (classical.some _) ∧ rk (classical.some _ n) = nat.find _), right.dcases_on (λ (h2 : set.partially_well_ordered_on.is_bad_seq r s (classical.some _)) (h3 : rk (classical.some _ n) = nat.find _), ⟨classical.some _, _⟩))
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
A version of Dickson's lemma any subset of functions
Π s : σ, α s is partially well
σ 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